let f, g be Function; :: thesis: ( dom f = NAT & f . 0 = X & ( for n being Nat holds f . (n + 1) = GrothendieckUniverse (f . n) ) & dom g = NAT & g . 0 = X & ( for n being Nat holds g . (n + 1) = GrothendieckUniverse (g . n) ) implies f = g )
assume that
A1: ( dom f = NAT & f . 0 = X & ( for n being Nat holds f . (n + 1) = GrothendieckUniverse (f . n) ) ) and
A2: ( dom g = NAT & g . 0 = X & ( for n being Nat holds g . (n + 1) = GrothendieckUniverse (g . n) ) ) ; :: thesis: f = g

now :: thesis: ( dom f = dom g & ( for x being object st x in NAT holds
f . x = g . x ) )

thus dom f = dom g by A1, A2; :: thesis: for x being object st x in NAT holds
f . x = g . x
defpred S₁[ Nat] means f . $1 = g . $1;
A3: S₁[ 0 ] by A1, A2;

now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
f . (k + 1) = GrothendieckUniverse (f . k) by A1
.= g . (k + 1) by A4, A2 ;
hence S₁[k + 1] ; :: thesis: verum

end;

then A5: for k being Nat st S₁[k] holds
S₁[k + 1] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A5);
hence for x being object st x in NAT holds
f . x = g . x ; :: thesis: verum

end;

hence f = g by A1, FUNCT_1:2; :: thesis: verum