defpred S₁[ Nat] means F₂() . $1 = F₃() . $1;
A8: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume F₂() . n = F₃() . n ; :: thesis: S₁[n + 1]
then A9: P₁[n,F₂() . n,F₃() . (n + 1)] by A6;
P₁[n,F₂() . n,F₂() . (n + 1)] by A3;
hence S₁[n + 1] by A7, A9; :: thesis: verum

end;

A10: S₁[ 0 ] by A2, A5;
for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A8);
then for x being object st x in NAT holds
F₂() . x = F₃() . x ;
hence F₂() = F₃() by A1, A4, FUNCT_1:2; :: thesis: verum