reconsider ff1 = f1, ff2 = f2 as Element of HFuncs NAT by Th31;
set n = len p;
reconsider z = ff1 . (Del p,i) as Element of NAT ;
defpred S₂[ Element of 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:37;
{} is PartFunc of (NAT * ),NAT by RELSET_1:25;
then {} in PFuncs (NAT * ),NAT by PARTFUN1:119;
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 Element of NAT
for x being Element of HFuncs NAT ex y being Element of HFuncs NAT st S₂[m,x,y]

proof

let m be Element of 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:37;
dom (B --> z) = B by FUNCOP_1:19;
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:32;
then len (p +* i,(m + 1)) = len p by FINSEQ_3:31;
then p +* i,(m + 1) is Element of (len p) -tuples_on NAT by FINSEQ_2:110;
then A7: B c= (len p) -tuples_on NAT by ZFMISC_1:37;
A8: x +* ({(p +* i,(m + 1))} --> (f2 . ((p +* i,m) ^ <*(x . (p +* i,m))*>))) = x +* (B --> z) ;

now

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 set ; :: 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:32;
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:31;
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, Th19, XBOOLE_1:8;
x +* ({(p +* i,(m + 1))} --> (f2 . ((p +* i,m) ^ <*(x . (p +* i,m))*>))) in PFuncs (NAT * ),NAT by A8, PARTFUN1:119;
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 Function of NAT ,(HFuncs NAT ) such that
A13: FF . 0 = A and
A14: for m being Element of NAT holds S₂[m,FF . m,FF . (m + 1)] from RECDEF_1:sch 2(A4);
take FF . (p /. i) ; :: thesis: ex F being Function of NAT ,(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 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 ) ) ) )
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 Element of 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 Element of 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