Axiom of Choice (Premise)

Use this premise to introduce the Axiom of Choice at the beginning
of a proof.

Where:

f    = family of sets 
i    = index set
f(j) = jth element of f
c(j) = choice from the jth element of f

1	ALL(f):ALL(i):[Set(f) & Set(i)
	& EXIST(a):a  i
	& ALL(a):[a  f => Set(a) & EXIST(b):b  a]
	& ALL(a):[a  i => f(a)  f]
	& ALL(a):[a  f => EXIST(b):[b  i & a=f(b)]]
	=> EXIST(c):ALL(a):[a  i => c(a)  f(a)]]
	Premise