reconsider ff2 = f2 as Element of HFuncs NAT by Th27;
let g1, g2 be Element of HFuncs NAT; :: thesis: ( ex F being sequence of (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 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 sequence of (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 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 sequence of (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 Nat holds S₁[m,F1 . m,F1 . (m + 1),p,i,f2] ; :: thesis: ( for F being sequence of (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 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 sequence of (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 Nat holds S₁[m,F2 . m,F2 . (m + 1),p,i,f2] ; :: thesis: g1 = g2
defpred S₂[ Nat] means F1 . $1 = F2 . $1;

A23: now :: thesis: for m being Nat st S₂[m] holds
S₂[m + 1]

let m be 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 Nat holds S₂[m] from NAT_1:sch 2(A25, A23);
hence g1 = g2 by A15, A19; :: thesis: verum