defpred S₁[ Nat] means F₂() . $1 = F₃() . $1;
A4: S₁[ 0 ] by B1, B2;
A5: 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 ( P₁[n,F₂() . n,F₂() . (n + 1)] & P₁[n,F₂() . n,F₃() . (n + 1)] ) by C1, C2;
hence S₁[n + 1] by A3; :: thesis: verum

end;

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