defpred S_{1}[ Nat] means ex S being non empty ManySortedSign st

( S = F_{3}() . $1 & P_{1}[S,F_{4}() . $1,$1] );

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

S_{1}[n + 1]
_{1}[ 0 ]
by A1;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A7, A4); :: thesis: verum

( S = F

A4: for n being Nat st S

S

proof

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

given S being non empty ManySortedSign such that A5: S = F_{3}() . n
and

A6: P_{1}[S,F_{4}() . n,n]
; :: thesis: S_{1}[n + 1]

take F_{1}(S,(F_{4}() . n),n)
; :: thesis: ( F_{1}(S,(F_{4}() . n),n) = F_{3}() . (n + 1) & P_{1}[F_{1}(S,(F_{4}() . n),n),F_{4}() . (n + 1),n + 1] )

F_{4}() . (n + 1) = F_{2}((F_{4}() . n),n)
by A2, A5;

hence ( F_{1}(S,(F_{4}() . n),n) = F_{3}() . (n + 1) & P_{1}[F_{1}(S,(F_{4}() . n),n),F_{4}() . (n + 1),n + 1] )
by A2, A3, A5, A6; :: thesis: verum

end;given S being non empty ManySortedSign such that A5: S = F

A6: P

take F

F

hence ( F

thus for n being Nat holds S