let n be Nat; :: thesis: Tarski-Class ((sequence_univers FinSETS) . n) = GrothendieckUniverse ((sequence_univers FinSETS) . n)

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

suppose n = 0 ; :: thesis: Tarski-Class ((sequence_univers FinSETS) . n) = GrothendieckUniverse ((sequence_univers FinSETS) . n)

then ( Tarski-Class ((sequence_univers FinSETS) . n) = SETS & GrothendieckUniverse ((sequence_univers FinSETS) . n) = SETS ) by Th77, Def9;
hence Tarski-Class ((sequence_univers FinSETS) . n) = GrothendieckUniverse ((sequence_univers FinSETS) . n) ; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: Tarski-Class ((sequence_univers FinSETS) . n) = GrothendieckUniverse ((sequence_univers FinSETS) . n)

then consider m being Nat such that
A1: n = m + 1 by NAT_1:6;
(sequence_univers FinSETS) . n = GrothendieckUniverse ((sequence_univers FinSETS) . m) by A1, Def9;
hence Tarski-Class ((sequence_univers FinSETS) . n) = GrothendieckUniverse ((sequence_univers FinSETS) . n) by CLASSES3:22; :: thesis: verum

end;

end;