let f1, f2 be Function-yielding primitive-recursive satisfying_primrec_conditions 1 -ary ManySortedSet of NAT ; :: thesis: ( f1 . 0 = 1 succ 1 & ( for m being Nat holds f1 . (m + 1) = primrec ((0 const (Ackermann (m,1))),((f1 . m) * <:<*(2 proj 2)*>:>),1) ) & f2 . 0 = 1 succ 1 & ( for m being Nat holds f2 . (m + 1) = primrec ((0 const (Ackermann (m,1))),((f2 . m) * <:<*(2 proj 2)*>:>),1) ) implies f1 = f2 )
assume that
A16: f1 . 0 = 1 succ 1 and
A17: for n being Nat holds f1 . (n + 1) = primrec ((0 const H₁(n,1)),((f1 . n) * <:<*(2 proj 2)*>:>),1) and
A18: f2 . 0 = 1 succ 1 and
A19: for n being Nat holds f2 . (n + 1) = primrec ((0 const H₁(n,1)),((f2 . n) * <:<*(2 proj 2)*>:>),1) ; :: thesis: f1 = f2
dom f1 = NAT by PARTFUN1:def 2;
hence dom f1 = dom f2 by PARTFUN1:def 2; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom f1 or f1 . b₁ = f2 . b₁ )
let n be object ; :: thesis: ( not n in dom f1 or f1 . n = f2 . n )
assume n in dom f1 ; :: thesis: f1 . n = f2 . n
then reconsider m = n as Nat ;
defpred S₁[ Nat] means f1 . $1 = f2 . $1;
A20: S₁[ 0 ] by A16, A18;
A21: 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 f2 . (n + 1) = primrec ((0 const H₁(n,1)),((f1 . n) * <:<*(2 proj 2)*>:>),1) by A19
.= f1 . (n + 1) by A17 ;
:: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A20, A21);
then S₁[m] ;
hence f1 . n = f2 . n ; :: thesis: verum