let f be Function of NAT,(union (rng sequence_univers)); :: thesis: f in super_univers
A1: not super_univers is trivial ;

now :: thesis: ( dom sequence_univers in super_univers & rng sequence_univers c= super_univers )

( dom sequence_univers = NAT & not super_univers is trivial ) by Def9;
hence dom sequence_univers in super_univers ; :: thesis: rng sequence_univers c= super_univers

now :: thesis: for x being object st x in rng sequence_univers holds
x in super_univers

let x be object ; :: thesis: ( x in rng sequence_univers implies b₁ in super_univers )
assume x in rng sequence_univers ; :: thesis: b₁ in super_univers
then consider y being object such that
A2: y in dom sequence_univers and
A3: x = sequence_univers . y by FUNCT_1:def 3;
reconsider y = y as Nat by A2;

per cases ( y = 0 or y <> 0 ) ;

suppose A4: y = 0 ; :: thesis: b₁ in super_univers

sequence_univers . 0 = {} by Def9;
hence x in super_univers by A4, A3, Th13; :: thesis: verum

end;

suppose y <> 0 ; :: thesis: b₁ in super_univers

then consider m being Nat such that
A5: y = m + 1 by NAT_1:6;
thus x in super_univers by A5, A3, Th104; :: thesis: verum

end;

end;

end;

hence rng sequence_univers c= super_univers ; :: thesis: verum

end;

then union (rng sequence_univers) in super_univers by CLASSES3:def 3;
then [:NAT,(union (rng sequence_univers)):] in super_univers by A1, CLASSES2:61;
hence f in super_univers by Th13; :: thesis: verum