reconsider ff2 = f2 as Element of HFuncs NAT by Th31;
let g1, g2 be Element of HFuncs NAT ; :: thesis: ( ex F being Function of NAT ,(HFuncs NAT ) st
( g1 = F . (p /. i) & ( i in dom p & Del p,i in dom f1 implies F . 0 = (p +* i,0 ) .--> (f1 . (Del p,i)) ) & ( ( not i in dom p or not Del p,i in dom f1 ) implies F . 0 = {} ) & ( for m being Element of NAT holds
( ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 implies F . (m + 1) = (F . m) +* ((p +* i,(m + 1)) .--> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) ) & ( ( not i in dom p or not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) ) & ex F being Function of NAT ,(HFuncs NAT ) st
( g2 = F . (p /. i) & ( i in dom p & Del p,i in dom f1 implies F . 0 = (p +* i,0 ) .--> (f1 . (Del p,i)) ) & ( ( not i in dom p or not Del p,i in dom f1 ) implies F . 0 = {} ) & ( for m being Element of NAT holds
( ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 implies F . (m + 1) = (F . m) +* ((p +* i,(m + 1)) .--> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) ) & ( ( not i in dom p or not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) ) implies g1 = g2 )
given F1 being Function of NAT ,(HFuncs NAT ) such that A15: g1 = F1 . (p /. i) and
A16: ( i in dom p & Del p,i in dom f1 implies F1 . 0 = (p +* i,0 ) .--> (f1 . (Del p,i)) ) and
A17: ( ( not i in dom p or not Del p,i in dom f1 ) implies F1 . 0 = {} ) and
A18: for m being Element of NAT holds S₁[m,F1 . m,F1 . (m + 1),p,i,f2] ; :: thesis: ( for F being Function of NAT ,(HFuncs NAT ) holds
( not g2 = F . (p /. i) or ( i in dom p & Del p,i in dom f1 & not F . 0 = (p +* i,0 ) .--> (f1 . (Del p,i)) ) or ( ( not i in dom p or not Del p,i in dom f1 ) & not F . 0 = {} ) or ex m being Element of NAT st
( ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 implies F . (m + 1) = (F . m) +* ((p +* i,(m + 1)) .--> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) ) implies ( ( not i in dom p or not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom f2 ) & not F . (m + 1) = F . m ) ) ) or g1 = g2 )
given F2 being Function of NAT ,(HFuncs NAT ) such that A19: g2 = F2 . (p /. i) and
A20: ( i in dom p & Del p,i in dom f1 implies F2 . 0 = (p +* i,0 ) .--> (f1 . (Del p,i)) ) and
A21: ( ( not i in dom p or not Del p,i in dom f1 ) implies F2 . 0 = {} ) and
A22: for m being Element of NAT holds S₁[m,F2 . m,F2 . (m + 1),p,i,f2] ; :: thesis: g1 = g2
defpred S₂[ Element of NAT ] means F1 . $1 = F2 . $1;

A23: now

let m be Element of NAT ; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume S₂[m] ; :: thesis: S₂[m + 1]
then A24: S₁[m,F1 . m,F2 . (m + 1),p,i,ff2] by A22;
S₁[m,F1 . m,F1 . (m + 1),p,i,f2] by A18;
hence S₂[m + 1] by A24; :: thesis: verum

end;

A25: S₂[ 0 ] by A16, A17, A20, A21;
for m being Element of NAT holds S₂[m] from NAT_1:sch 1(A25, A23);
hence g1 = g2 by A15, A19; :: thesis: verum