let n be Nat; :: thesis: (sequence_univers FinSETS) . n = UNIVERSE n
defpred S₁[ Nat] means (sequence_univers FinSETS) . $1 = UNIVERSE $1;
A1: S₁[ 0 ] by Def9, CLASSES2:65;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( (sequence_univers FinSETS) . (k + 1) = GrothendieckUniverse ((sequence_univers FinSETS) . k) & UNIVERSE (k + 1) = Tarski-Class ((sequence_univers FinSETS) . k) )

thus (sequence_univers FinSETS) . (k + 1) = GrothendieckUniverse ((sequence_univers FinSETS) . k) by Def9; :: thesis: UNIVERSE (k + 1) = Tarski-Class ((sequence_univers FinSETS) . k)
succ (Segm k) = Segm (k + 1) by NAT_1:38;
hence UNIVERSE (k + 1) = Tarski-Class ((sequence_univers FinSETS) . k) by A3, CLASSES2:66; :: thesis: verum

end;

hence S₁[k + 1] by Th98; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence (sequence_univers FinSETS) . n = UNIVERSE n ; :: thesis: verum