defpred S₁[ Nat] means GrothendieckUniverse ((sequence_univers {}) . $1) = (sequence_univers (GrothendieckUniverse {})) . $1;
A1: S₁[ 0 ]

proof

( GrothendieckUniverse ((sequence_univers {}) . 0) = GrothendieckUniverse {} & (sequence_univers (GrothendieckUniverse {})) . 0 = GrothendieckUniverse {} ) by Def9;
hence S₁[ 0 ] ; :: thesis: verum

end;

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]
( GrothendieckUniverse ((sequence_univers {}) . (k + 1)) = GrothendieckUniverse (GrothendieckUniverse ((sequence_univers {}) . k)) & (sequence_univers (GrothendieckUniverse {})) . (k + 1) = GrothendieckUniverse ((sequence_univers (GrothendieckUniverse {})) . k) ) by Def9;
hence S₁[k + 1] by A3; :: thesis: verum

end;

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