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 S2[ Nat, Element of HFuncs NAT, Element of HFuncs NAT] means S1[$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 S2[m,x,y]
proof
let m be
Nat;
for x being Element of HFuncs NAT ex y being Element of HFuncs NAT st S2[m,x,y]let x be
Element of
HFuncs NAT;
ex y being Element of HFuncs NAT st S2[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 ( 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
;
x +* ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*(x . (p +* (i,m)))*>))) in HFuncs NAT
dom x c= (len p) -tuples_on NAT
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;
verum end;
then reconsider y =
y as
Element of
HFuncs NAT by A5;
take
y
;
S2[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;
( ( 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;
verum
end;
consider FF being sequence of (HFuncs NAT) such that
A13:
FF . 0 = A
and
A14:
for m being Nat holds S2[m,FF . m,FF . (m + 1)]
from RECDEF_1:sch 2(A4);
take
FF . (p /. i)
; 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
; ( 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; verum