set g = the Choice of ComplUniverse ;
A1: dom the Choice of ComplUniverse = dom ComplUniverse by ORDERS_1:def 1
.= NAT by FUNCT_2:def 1 ;
rng the Choice of ComplUniverse c= union (union (rng sequence_univers))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng the Choice of ComplUniverse or x in union (union (rng sequence_univers)) )
assume x in rng the Choice of ComplUniverse ; :: thesis: x in union (union (rng sequence_univers))
then consider y being object such that
A2: y in dom the Choice of ComplUniverse and
A3: x = the Choice of ComplUniverse . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A1, A2;
A4: not ComplUniverse . y is empty by Th109;
y in dom ComplUniverse by A1, A2, FUNCT_2:def 1;
then x = the Element of ComplUniverse . y by A3, ORDERS_1:def 1;
then A5: x in ComplUniverse . y by A4;
A6: UNIVERSE ((y + 1) + 1) is axiom_GU1 ;
A7: UNIVERSE (y + 1) in UNIVERSE ((y + 1) + 1) by Th99;
A8: UNIVERSE ((y + 1) + 1) c= union (rng sequence_univers)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UNIVERSE ((y + 1) + 1) or x in union (rng sequence_univers) )
assume A9: x in UNIVERSE ((y + 1) + 1) ; :: thesis: x in union (rng sequence_univers)
set n = (y + 1) + 1;
(((y + 1) + 1) + 1) + 1 in NAT ;
then A10: (((y + 1) + 1) + 1) + 1 in dom sequence_univers by Def9;
A11: ( x in sequence_univers . (((y + 1) + 1) + 1) & sequence_univers . (((y + 1) + 1) + 1) c= sequence_univers . ((((y + 1) + 1) + 1) + 1) ) by Th102, A9, Th105;
sequence_univers . ((((y + 1) + 1) + 1) + 1) in rng sequence_univers by A10, FUNCT_1:def 3;
hence x in union (rng sequence_univers) by A11, TARSKI:def 4; :: thesis: verum

end;

reconsider z1 = UNIVERSE (y + 1) as Element of UNIVERSE ((y + 1) + 1) by Th99;
UNIVERSE y in UNIVERSE (y + 1) by Th99;
then reconsider z2 = UNIVERSE y as Element of UNIVERSE ((y + 1) + 1) by A6, A7;
A12: x in z1 \ z2 by A5, Def14;
( x in union (UNIVERSE ((y + 1) + 1)) & union (UNIVERSE ((y + 1) + 1)) c= union (union (rng sequence_univers)) ) by A12, A8, ZFMISC_1:77, TARSKI:def 4;
hence x in union (union (rng sequence_univers)) ; :: thesis: verum

end;

then reconsider g = the Choice of ComplUniverse as Function of NAT,(union (union (rng sequence_univers))) by A1, FUNCT_2:2;
take g ; :: thesis: for i being Nat holds g . i in ComplUniverse . i
for i being Nat holds g . i in ComplUniverse . i

proof

let i be Nat; :: thesis: g . i in ComplUniverse . i
dom ComplUniverse = NAT by FUNCT_2:def 1;
then g . i = the Element of ComplUniverse . i by ORDERS_1:def 1, ORDINAL1:def 12;
then ( g . i is Element of ComplUniverse . i & not ComplUniverse . i is empty ) by Th109;
hence g . i in ComplUniverse . i ; :: thesis: verum

end;

hence for i being Nat holds g . i in ComplUniverse . i ; :: thesis: verum