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 S1[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 S1[m,F2 . m,F2 . (m + 1),p,i,f2] ; :: thesis: g1 = g2
defpred S2[ Nat] means F1 . $1 = F2 . $1;
A23: now :: thesis: for m being Nat st S2[m] holds
S2[m + 1]
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume S2[m] ; :: thesis: S2[m + 1]
then A24: S1[m,F1 . m,F2 . (m + 1),p,i,ff2] by A22;
S1[m,F1 . m,F1 . (m + 1),p,i,f2] by A18;
hence S2[m + 1] by A24; :: thesis: verum
end;
A25: S2[ 0 ] by A16, A17, A20, A21;
for m being Nat holds S2[m] from NAT_1:sch 2(A25, A23);
 hence g1 = g2 by A15, A19; :: thesis: verum