let n be Nat; :: thesis: sequence_univers . (n + 1) in GrothendieckUniverse sequence_univers
set SU = GrothendieckUniverse sequence_univers;

now :: thesis: ( n + 1 in dom sequence_univers & sequence_univers . 1 = FinSETS & sequence_univers . (n + 1) = UNIVERSE n )

n + 1 in NAT ;
hence n + 1 in dom sequence_univers by Def9; :: thesis: ( sequence_univers . 1 = FinSETS & sequence_univers . (n + 1) = UNIVERSE n )
set f = sequence_univers ;
A1: ( dom sequence_univers = NAT & sequence_univers . 0 = {} & ( for n being Nat holds sequence_univers . (n + 1) = GrothendieckUniverse (sequence_univers . n) ) ) by Def9;
thus sequence_univers . 1 = sequence_univers . (0 + 1)
.= GrothendieckUniverse {} by A1
.= FinSETS by Th45, CLASSES2:56, CLASSES3:21 ; :: thesis: sequence_univers . (n + 1) = UNIVERSE n
thus sequence_univers . (n + 1) = UNIVERSE n by Th102; :: thesis: verum

end;

then ( [(n + 1),(sequence_univers . (n + 1))] in sequence_univers & sequence_univers in GrothendieckUniverse sequence_univers & GrothendieckUniverse sequence_univers is axiom_GU1 ) by CLASSES3:def 4, FUNCT_1:1;
then reconsider x = [(n + 1),(sequence_univers . (n + 1))] as pair Element of GrothendieckUniverse sequence_univers ;
x `2 is Element of GrothendieckUniverse sequence_univers ;
hence sequence_univers . (n + 1) in GrothendieckUniverse sequence_univers ; :: thesis: verum