let V, A be set ; :: thesis: for m, n being Nat st m <> 0 & m <= n holds
(FNDSC (V,A)) . m c= (FNDSC (V,A)) . n
let m, n be Nat; :: thesis: ( m <> 0 & m <= n implies (FNDSC (V,A)) . m c= (FNDSC (V,A)) . n )
assume A1: m <> 0 ; :: thesis: ( not m <= n or (FNDSC (V,A)) . m c= (FNDSC (V,A)) . n )
set S = FNDSC (V,A);
defpred S1[ Nat] means ( m <= $1 implies (FNDSC (V,A)) . m c= (FNDSC (V,A)) . $1 );
A2: S1[ 0 ] ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
assume A5: m <= k + 1 ; :: thesis: (FNDSC (V,A)) . m c= (FNDSC (V,A)) . (k + 1)
per cases ( m = k + 1 or m <= k ) by A5, NAT_1:8;
suppose m = k + 1 ; :: thesis: (FNDSC (V,A)) . m c= (FNDSC (V,A)) . (k + 1)
hence (FNDSC (V,A)) . m c= (FNDSC (V,A)) . (k + 1) ; :: thesis: verum
end;
suppose A6: m <= k ; :: thesis: (FNDSC (V,A)) . m c= (FNDSC (V,A)) . (k + 1)
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: (FNDSC (V,A)) . m c= (FNDSC (V,A)) . (k + 1)
hence (FNDSC (V,A)) . m c= (FNDSC (V,A)) . (k + 1) by A1, A6; :: thesis: verum
end;
suppose A7: k <> 0 ; :: thesis: (FNDSC (V,A)) . m c= (FNDSC (V,A)) . (k + 1)
defpred S2[ Nat] means ( $1 <> 0 implies (FNDSC (V,A)) . $1 c= (FNDSC (V,A)) . ($1 + 1) );
A8: S2[ 0 ] ;
A9: for z being Nat st S2[z] holds
S2[z + 1]
proof
let z be Nat; :: thesis: ( S2[z] implies S2[z + 1] )
assume A10: S2[z] ; :: thesis: S2[z + 1]
per cases ( z = 0 or z <> 0 ) ;
suppose A11: z = 0 ; :: thesis: S2[z + 1]
A12: (FNDSC (V,A)) . 1 = NDSS (V,A) by Th9;
(FNDSC (V,A)) . (1 + 1) = NDSS (V,(A \/ (NDSS (V,A)))) by Th10;
hence S2[z + 1] by A11, A12, Th7, XBOOLE_1:7; :: thesis: verum
end;
suppose z <> 0 ; :: thesis: S2[z + 1]
then A13: A \/ ((FNDSC (V,A)) . z) c= A \/ ((FNDSC (V,A)) . (z + 1)) by A10, XBOOLE_1:9;
A14: (FNDSC (V,A)) . (z + 1) = NDSS (V,(A \/ ((FNDSC (V,A)) . z))) by Def3;
(FNDSC (V,A)) . ((z + 1) + 1) = NDSS (V,(A \/ ((FNDSC (V,A)) . (z + 1)))) by Def3;
hence S2[z + 1] by A13, A14, Th7; :: thesis: verum
end;
end;
end;
for z being Nat holds S2[z] from NAT_1:sch 2(A8, A9);
then (FNDSC (V,A)) . k c= (FNDSC (V,A)) . (k + 1) by A7;
hence (FNDSC (V,A)) . m c= (FNDSC (V,A)) . (k + 1) by A4, A6; :: thesis: verum
end;
end;
end;
end;
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A2, A3);
 hence ( not m <= n or (FNDSC (V,A)) . m c= (FNDSC (V,A)) . n ) ; :: thesis: verum