deffunc H₁( Element of NAT ) -> Element of bool (UNIVERSE ($1 + 1)) = (UNIVERSE ($1 + 1)) \ (UNIVERSE $1);
consider f being Function such that
A1: dom f = NAT and
A2: for n being Element of NAT st n in NAT holds
f . n = H₁(n) from CLASSES1:sch 2();
rng f c= union (rng sequence_univers)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in union (rng sequence_univers) )
assume x in rng f ; :: thesis: x in union (rng sequence_univers)
then consider y being object such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A1, A3;
A5: UNIVERSE ((y + 1) + 1) is axiom_GU1 ;
A6: UNIVERSE (y + 1) in UNIVERSE ((y + 1) + 1) by Th99;
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 A5, A6;
A7: x = z1 \ z2 by A2, A4;
UNIVERSE ((y + 1) + 1) in rng sequence_univers

proof

set n = (y + 1) + 1;
((y + 1) + 1) + 1 in NAT ;
then A8: ((y + 1) + 1) + 1 in dom sequence_univers by Def9;
sequence_univers . (((y + 1) + 1) + 1) = UNIVERSE ((y + 1) + 1) by Th102;
hence UNIVERSE ((y + 1) + 1) in rng sequence_univers by A8, FUNCT_1:def 3; :: thesis: verum

end;

hence x in union (rng sequence_univers) by A7, TARSKI:def 4; :: thesis: verum

end;

then reconsider f = f as Function of NAT,(union (rng sequence_univers)) by A1, FUNCT_2:2;
take f ; :: thesis: for n being Nat holds f . n = (UNIVERSE (n + 1)) \ (UNIVERSE n)

now :: thesis: for i being Nat holds f . i = (UNIVERSE (i + 1)) \ (UNIVERSE i)

let i be Nat; :: thesis: f . i = (UNIVERSE (i + 1)) \ (UNIVERSE i)
i is Element of NAT by ORDINAL1:def 12;
hence f . i = (UNIVERSE (i + 1)) \ (UNIVERSE i) by A2; :: thesis: verum

end;

hence for n being Nat holds f . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) ; :: thesis: verum