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

proof

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

end;

A10: S₁[ 0 ] by A2, A5;
for n being Nat holds S₁[n]

proof

let n be Nat; :: thesis: S₁[n]
thus S₁[n] from ORDINAL2:sch 17(A10, A8); :: thesis: verum

end;

then for x being object st x in omega holds
F₂() . x = F₃() . x ;
hence F₂() = F₃() by A1, A4, FUNCT_1:2; :: thesis: verum