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)))*>
defpred S₁[ Nat] means ( $1 in dom (apply p,x) implies (apply (p ^ <*f*>),x) . $1 = (apply p,x) . $1 );
A1: len (apply p,x) = (len p) + 1 by Def5;
A2: (apply p,x) . 1 = x by Def5;
A3: 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
A4: ( i in dom (apply p,x) implies (apply (p ^ <*f*>),x) . i = (apply p,x) . i ) and
A5: i + 1 in dom (apply p,x) ; :: thesis: (apply (p ^ <*f*>),x) . (i + 1) = (apply p,x) . (i + 1)
A6: i + 1 <= len (apply p,x) by A5, FINSEQ_3:27;
then A7: i <= len (apply p,x) by NAT_1:13;
A8: i <= len p by A1, A6, XREAL_1:8;

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 A9: i > 0 ; :: thesis: (apply (p ^ <*f*>),x) . (i + 1) = (apply p,x) . (i + 1)

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

end;

end;

end;

A12: S₁[ 0 ] by FINSEQ_3:27;
A13: for i being Nat holds S₁[i] from NAT_1:sch 2(A12, A3);
len <*f*> = 1 by FINSEQ_1:57;
then A14: len (p ^ <*f*>) = (len p) + 1 by FINSEQ_1:35;
A15: (len p) + 1 >= 1 by NAT_1:11;
then A16: ( (p ^ <*f*>) . ((len p) + 1) = f & (len p) + 1 in dom (p ^ <*f*>) ) by A14, FINSEQ_1:59, FINSEQ_3:27;
A17: (len p) + 1 in dom (apply p,x) by A1, A15, FINSEQ_3:27;

A18: 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 A19: i = 1 by FINSEQ_1:4, TARSKI:def 1;
then ( f . ((apply (p ^ <*f*>),x) . ((len p) + i)) = (apply (p ^ <*f*>),x) . ((len (apply p,x)) + i) & (apply (p ^ <*f*>),x) . ((len p) + i) = (apply p,x) . ((len p) + i) ) by A1, A16, A17, A13, Def5;
hence (apply (p ^ <*f*>),x) . ((len (apply p,x)) + i) = <*(f . ((apply p,x) . ((len p) + 1)))*> . i by A19, FINSEQ_1:57; :: thesis: verum

end;

len (apply (p ^ <*f*>),x) = (len (p ^ <*f*>)) + 1 by Def5;
then ( len <*(f . ((apply p,x) . ((len p) + 1)))*> = 1 & dom (apply (p ^ <*f*>),x) = Seg ((len (apply p,x)) + 1) ) by A1, A14, FINSEQ_1:57, FINSEQ_1:def 3;
hence apply (p ^ <*f*>),x = (apply p,x) ^ <*(f . ((apply p,x) . ((len p) + 1)))*> by A13, A18, FINSEQ_1:def 7; :: thesis: verum