let f, g be Function; :: thesis: ( dom f = NAT & f . 0 = A & ( for n being Nat holds f . (n + 1) = NDSS (V,(A \/ (f . n))) ) & dom g = NAT & g . 0 = A & ( for n being Nat holds g . (n + 1) = NDSS (V,(A \/ (g . n))) ) implies f = g )
assume that
A1: dom f = NAT and
A2: f . 0 = A and
A3: for n being Nat holds f . (n + 1) = NDSS (V,(A \/ (f . n))) and
A4: dom g = NAT and
A5: g . 0 = A and
A6: for n being Nat holds g . (n + 1) = NDSS (V,(A \/ (g . n))) ; :: thesis: f = g
thus dom f = dom g by A1, A4; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom f or f . b₁ = g . b₁ )
let x be object ; :: thesis: ( not x in dom f or f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
then reconsider n = x as Element of NAT by A1;
defpred S₁[ Nat] means f . $1 = g . $1;
A7: S₁[ 0 ] by A2, A5;
A8: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
hence g . (n + 1) = NDSS (V,(A \/ (f . n))) by A6
.= f . (n + 1) by A3 ;
:: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A8);
then f . n = g . n ;
hence f . x = g . x ; :: thesis: verum