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_{1} being object holds

( not b_{1} in dom f or f . b_{1} = g . b_{1} )

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_{1}[ Nat] means f . $1 = g . $1;

A7: S_{1}[ 0 ]
by A2, A5;

A8: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A7, A8);

then f . n = g . n ;

hence f . x = g . x ; :: thesis: verum

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

( not 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

A7: S

A8: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume S_{1}[n]
; :: thesis: S_{1}[n + 1]

hence g . (n + 1) = NDSS (V,(A \/ (f . n))) by A6

.= f . (n + 1) by A3 ;

:: thesis: verum

end;assume S

hence g . (n + 1) = NDSS (V,(A \/ (f . n))) by A6

.= f . (n + 1) by A3 ;

:: thesis: verum

then f . n = g . n ;

hence f . x = g . x ; :: thesis: verum