set SU = GrothendieckUniverse sequence_univers;

now :: thesis: ( 1 in dom sequence_univers & 2 in dom sequence_univers & sequence_univers . 1 = FinSETS & sequence_univers . 2 = SETS )

( 1 in NAT & 2 in NAT ) ;
hence ( 1 in dom sequence_univers & 2 in dom sequence_univers ) by Def9; :: thesis: ( sequence_univers . 1 = FinSETS & sequence_univers . 2 = SETS )
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 A2: sequence_univers . 1 = sequence_univers . (0 + 1)
.= GrothendieckUniverse {} by A1
.= FinSETS by Th45, CLASSES2:56, CLASSES3:21 ; :: thesis: sequence_univers . 2 = SETS
thus sequence_univers . 2 = sequence_univers . (1 + 1)
.= SETS by Th77, A2, Def9 ; :: thesis: verum

end;

then ( [1,FinSETS] in sequence_univers & [2,SETS] 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 = [1,FinSETS], y = [2,SETS] as pair Element of GrothendieckUniverse sequence_univers ;
( x `2 is Element of GrothendieckUniverse sequence_univers & y `2 is Element of GrothendieckUniverse sequence_univers ) ;
hence ( FinSETS in GrothendieckUniverse sequence_univers & SETS in GrothendieckUniverse sequence_univers ) ; :: thesis: verum