let x be object ; :: 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 Def4;
A2: (apply (p,x)) . 1 = x by Def4;
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:25;
then A7: i <= len (apply (p,x)) by NAT_1:13;
A8: i <= len p by A1, A6, XREAL_1:6;

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, Def4; :: 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:25;
then ( dom p c= dom (p ^ <*f*>) & g = (p ^ <*f*>) . i ) by FINSEQ_1:26, FINSEQ_1:def 7;
then (apply ((p ^ <*f*>),x)) . (i + 1) = g . ((apply ((p ^ <*f*>),x)) . i) by A11, Def4;
hence (apply ((p ^ <*f*>),x)) . (i + 1) = (apply (p,x)) . (i + 1) by A4, A7, A10, A11, Def4, FINSEQ_3:25; :: thesis: verum

end;

end;

end;

A12: S₁[ 0 ] by FINSEQ_3:25;
A13: for i being Nat holds S₁[i] from NAT_1:sch 2(A12, A3);
len <*f*> = 1 by FINSEQ_1:40;
then A14: len (p ^ <*f*>) = (len p) + 1 by FINSEQ_1:22;
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:42, FINSEQ_3:25;
A17: (len p) + 1 in dom (apply (p,x)) by A1, A15, FINSEQ_3:25;

A18: now :: thesis: for i being Nat st i in dom <*(f . ((apply (p,x)) . ((len p) + 1)))*> holds
(apply ((p ^ <*f*>),x)) . ((len (apply (p,x))) + i) = <*(f . ((apply (p,x)) . ((len p) + 1)))*> . i

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:38;
then A19: i = 1 by FINSEQ_1:2, 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, Def4;
hence (apply ((p ^ <*f*>),x)) . ((len (apply (p,x))) + i) = <*(f . ((apply (p,x)) . ((len p) + 1)))*> . i by A19; :: thesis: verum

end;

len (apply ((p ^ <*f*>),x)) = (len (p ^ <*f*>)) + 1 by Def4;
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:40, 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