defpred S1[ Nat] means F2() . $1 = F3() . $1;
A8:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume
F2()
. n = F3()
. n
;
S1[n + 1]
then A9:
P1[
n,
F2()
. n,
F3()
. (n + 1)]
by A6;
P1[
n,
F2()
. n,
F2()
. (n + 1)]
by A3;
hence
S1[
n + 1]
by A7, A9;
verum
end;
A10:
S1[ 0 ]
by A2, A5;
for n being Nat holds S1[n]
from NAT_1:sch 2(A10, A8);
then
for x being object st x in NAT holds
F2() . x = F3() . x
;
hence
F2() = F3()
by A1, A4, FUNCT_1:2; verum