reconsider ff1 = f1, ff2 = f2 as Element of HFuncs NAT by Th27;
set n = len p;
reconsider z = ff1 . (Del (p,i)) as Element of NAT ;
defpred S₂[ Nat, Element of HFuncs NAT, Element of HFuncs NAT] means S₁[$1,$2,$3,p,i,ff2];
p +* (i,0) in NAT * by FINSEQ_1:def 11;
then reconsider Ap = {(p +* (i,0))} as non empty Subset of (NAT *) by ZFMISC_1:31;
{} is PartFunc of (NAT *),NAT by RELSET_1:12;
then {} in PFuncs ((NAT *),NAT) by PARTFUN1:45;
then A1: {} in HFuncs NAT ;
Ap --> z = (p +* (i,0)) .--> z ;
then Ap --> z in HFuncs NAT ;
then reconsider t = Ap --> z, e = {} as Element of HFuncs NAT by A1;
( ( i in dom p & Del (p,i) in dom f1 ) or not i in dom p or not Del (p,i) in dom f1 ) ;
then consider A being Element of HFuncs NAT such that
A2: ( i in dom p & Del (p,i) in dom f1 implies A = t ) and
A3: ( ( not i in dom p or not Del (p,i) in dom f1 ) implies A = e ) ;
A4: for m being Nat
for x being Element of HFuncs NAT ex y being Element of HFuncs NAT st S₂[m,x,y]

proof

let m be Nat; :: thesis: for x being Element of HFuncs NAT ex y being Element of HFuncs NAT st S₂[m,x,y]
let x be Element of HFuncs NAT; :: thesis: ex y being Element of HFuncs NAT st S₂[m,x,y]
set f = x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>)));
reconsider z = ff2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>) as Element of NAT ;
( ( i in dom p & p +* (i,m) in dom x & (p +* (i,m)) ^ <*(x . (p +* (i,m)))*> in dom f2 ) or not i in dom p or not p +* (i,m) in dom x or not (p +* (i,m)) ^ <*(x . (p +* (i,m)))*> in dom f2 ) ;
then consider y being Function such that
A5: ( ( i in dom p & p +* (i,m) in dom x & (p +* (i,m)) ^ <*(x . (p +* (i,m)))*> in dom f2 & y = x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))) ) or ( ( not i in dom p or not p +* (i,m) in dom x or not (p +* (i,m)) ^ <*(x . (p +* (i,m)))*> in dom f2 ) & y = x ) ) ;
p +* (i,(m + 1)) in NAT * by FINSEQ_1:def 11;
then reconsider B = {(p +* (i,(m + 1)))} as Subset of (NAT *) by ZFMISC_1:31;
dom (B --> z) = B ;
then A6: dom (x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>)))) = (dom x) \/ B by FUNCT_4:def 1;
dom p = dom (p +* (i,(m + 1))) by FUNCT_7:30;
then len (p +* (i,(m + 1))) = len p by FINSEQ_3:29;
then p +* (i,(m + 1)) is Element of (len p) -tuples_on NAT by FINSEQ_2:92;
then A7: B c= (len p) -tuples_on NAT by ZFMISC_1:31;
A8: x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))) = x +* (B --> z) ;

now :: thesis: ( p +* (i,m) in dom x implies x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))) in HFuncs NAT )

assume A9: p +* (i,m) in dom x ; :: thesis: x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))) in HFuncs NAT
dom x c= (len p) -tuples_on NAT

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom x or a in (len p) -tuples_on NAT )
A10: dom p = dom (p +* (i,m)) by FUNCT_7:30;
assume A11: a in dom x ; :: thesis: a in (len p) -tuples_on NAT
then reconsider q = a as Element of NAT * ;
len q = len (p +* (i,m)) by A9, A11, MARGREL1:def 1;
then len q = len p by A10, FINSEQ_3:29;
hence a in (len p) -tuples_on NAT ; :: thesis: verum

end;

then A12: x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))) is homogeneous by A7, A6, Th15, XBOOLE_1:8;
x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))) in PFuncs ((NAT *),NAT) by A8, PARTFUN1:45;
hence x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))) in HFuncs NAT by A12; :: thesis: verum

end;

then reconsider y = y as Element of HFuncs NAT by A5;
take y ; :: thesis: S₂[m,x,y]
thus ( i in dom p & p +* (i,m) in dom x & (p +* (i,m)) ^ <*(x . (p +* (i,m)))*> in dom ff2 implies y = x +* ((p +* (i,(m + 1))) .--> (ff2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))) ) by A5; :: thesis: ( ( not i in dom p or not p +* (i,m) in dom x or not (p +* (i,m)) ^ <*(x . (p +* (i,m)))*> in dom ff2 ) implies y = x )
thus ( ( not i in dom p or not p +* (i,m) in dom x or not (p +* (i,m)) ^ <*(x . (p +* (i,m)))*> in dom ff2 ) implies y = x ) by A5; :: thesis: verum

end;

consider FF being sequence of (HFuncs NAT) such that
A13: FF . 0 = A and
A14: for m being Nat holds S₂[m,FF . m,FF . (m + 1)] from RECDEF_1:sch 2(A4);
take FF . (p /. i) ; :: thesis: ex F being sequence of (HFuncs NAT) st
( FF . (p /. i) = 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 ) ) ) )
take FF ; :: thesis: ( FF . (p /. i) = FF . (p /. i) & ( i in dom p & Del (p,i) in dom f1 implies FF . 0 = (p +* (i,0)) .--> (f1 . (Del (p,i))) ) & ( ( not i in dom p or not Del (p,i) in dom f1 ) implies FF . 0 = {} ) & ( for m being Nat holds
( ( i in dom p & p +* (i,m) in dom (FF . m) & (p +* (i,m)) ^ <*((FF . m) . (p +* (i,m)))*> in dom f2 implies FF . (m + 1) = (FF . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((FF . m) . (p +* (i,m)))*>))) ) & ( ( not i in dom p or not p +* (i,m) in dom (FF . m) or not (p +* (i,m)) ^ <*((FF . m) . (p +* (i,m)))*> in dom f2 ) implies FF . (m + 1) = FF . m ) ) ) )
thus ( FF . (p /. i) = FF . (p /. i) & ( i in dom p & Del (p,i) in dom f1 implies FF . 0 = (p +* (i,0)) .--> (f1 . (Del (p,i))) ) & ( ( not i in dom p or not Del (p,i) in dom f1 ) implies FF . 0 = {} ) & ( for m being Nat holds
( ( i in dom p & p +* (i,m) in dom (FF . m) & (p +* (i,m)) ^ <*((FF . m) . (p +* (i,m)))*> in dom f2 implies FF . (m + 1) = (FF . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((FF . m) . (p +* (i,m)))*>))) ) & ( ( not i in dom p or not p +* (i,m) in dom (FF . m) or not (p +* (i,m)) ^ <*((FF . m) . (p +* (i,m)))*> in dom f2 ) implies FF . (m + 1) = FF . m ) ) ) ) by A2, A3, A13, A14; :: thesis: verum