let x be set ; :: thesis: for p being Function-yielding FinSequence
for f being Function holds apply (p ^ <*f*>),x = (apply p,x) ^ <*(f . ((apply p,x) . ((len p) + 1)))*>
let p be Function-yielding FinSequence; :: thesis: for f being Function holds apply (p ^ <*f*>),x = (apply p,x) ^ <*(f . ((apply p,x) . ((len p) + 1)))*>
let f be Function; :: thesis: apply (p ^ <*f*>),x = (apply p,x) ^ <*(f . ((apply p,x) . ((len p) + 1)))*>
A1: ( len (apply (p ^ <*f*>),x) = (len (p ^ <*f*>)) + 1 & (apply (p ^ <*f*>),x) . 1 = x & ( for i being Element of NAT
for g being Function st i in dom (p ^ <*f*>) & g = (p ^ <*f*>) . i holds
(apply (p ^ <*f*>),x) . (i + 1) = g . ((apply (p ^ <*f*>),x) . i) ) ) by Def5;
A2: ( len (apply p,x) = (len p) + 1 & (apply p,x) . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
(apply p,x) . (i + 1) = f . ((apply p,x) . i) ) ) by Def5;
len <*f*> = 1 by FINSEQ_1:57;
then A3: ( len (p ^ <*f*>) = (len p) + 1 & len <*(f . ((apply p,x) . ((len p) + 1)))*> = 1 ) by FINSEQ_1:35, FINSEQ_1:57;
then A4: dom (apply (p ^ <*f*>),x) = Seg ((len (apply p,x)) + 1) by A1, A2, FINSEQ_1:def 3;
A5: (p ^ <*f*>) . ((len p) + 1) = f by FINSEQ_1:59;
(len p) + 1 >= 1 by NAT_1:11;
then A6: ( (len p) + 1 in dom (p ^ <*f*>) & (len p) + 1 in dom (apply p,x) ) by A2, A3, FINSEQ_3:27;
defpred S₁[ Nat] means ( $1 in dom (apply p,x) implies (apply (p ^ <*f*>),x) . $1 = (apply p,x) . $1 );
A7: S₁[ 0 ] by FINSEQ_3:27;
A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A9: ( i in dom (apply p,x) implies (apply (p ^ <*f*>),x) . i = (apply p,x) . i ) and
A10: i + 1 in dom (apply p,x) ; :: thesis: (apply (p ^ <*f*>),x) . (i + 1) = (apply p,x) . (i + 1)
( i <= i + 1 & i + 1 <= len (apply p,x) ) by A10, FINSEQ_3:27, NAT_1:13;
then A11: ( i <= len (apply p,x) & i <= len p ) by A2, XREAL_1:8, XXREAL_0:2;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: (apply (p ^ <*f*>),x) . (i + 1) = (apply p,x) . (i + 1)

hence (apply (p ^ <*f*>),x) . (i + 1) = (apply p,x) . (i + 1) by A2, Def5; :: thesis: verum

end;

suppose i > 0 ; :: thesis: (apply (p ^ <*f*>),x) . (i + 1) = (apply p,x) . (i + 1)

then A12: i >= 0 + 1 by NAT_1:13;
then A13: ( i in dom (apply p,x) & i in dom p ) by A11, FINSEQ_3:27;
reconsider g = p . i as Function ;
dom p c= dom (p ^ <*f*>) by FINSEQ_1:39;
then ( i in dom (p ^ <*f*>) & g = (p ^ <*f*>) . i ) by A13, FINSEQ_1:def 7;
then ( (apply (p ^ <*f*>),x) . (i + 1) = g . ((apply (p ^ <*f*>),x) . i) & (apply p,x) . (i + 1) = g . ((apply p,x) . i) ) by A13, Def5;
hence (apply (p ^ <*f*>),x) . (i + 1) = (apply p,x) . (i + 1) by A9, A11, A12, FINSEQ_3:27; :: thesis: verum

end;

end;

end;

A14: for i being Nat holds S₁[i] from NAT_1:sch 2(A7, A8);

now

let i be Nat; :: thesis: ( i in dom <*(f . ((apply p,x) . ((len p) + 1)))*> implies (apply (p ^ <*f*>),x) . ((len (apply p,x)) + i) = <*(f . ((apply p,x) . ((len p) + 1)))*> . i )
assume i in dom <*(f . ((apply p,x) . ((len p) + 1)))*> ; :: thesis: (apply (p ^ <*f*>),x) . ((len (apply p,x)) + i) = <*(f . ((apply p,x) . ((len p) + 1)))*> . i
then i in Seg 1 by FINSEQ_1:55;
then A15: i = 1 by FINSEQ_1:4, TARSKI:def 1;
then A16: f . ((apply (p ^ <*f*>),x) . ((len p) + i)) = (apply (p ^ <*f*>),x) . ((len (apply p,x)) + i) by A2, A5, A6, Def5;
(apply (p ^ <*f*>),x) . ((len p) + i) = (apply p,x) . ((len p) + i) by A6, A14, A15;
hence (apply (p ^ <*f*>),x) . ((len (apply p,x)) + i) = <*(f . ((apply p,x) . ((len p) + 1)))*> . i by A15, A16, FINSEQ_1:57; :: thesis: verum

end;

hence apply (p ^ <*f*>),x = (apply p,x) ^ <*(f . ((apply p,x) . ((len p) + 1)))*> by A3, A4, A14, FINSEQ_1:def 7; :: thesis: verum