let D, E be non empty set ; :: thesis: for h being Function of D,E
for p being FinSequence of D
for d being Element of D holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
let h be Function of D,E; :: thesis: for p being FinSequence of D
for d being Element of D holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
let p be FinSequence of D; :: thesis: for d being Element of D holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
let d be Element of D; :: thesis: h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
set q = h * (p ^ <*d*>);
set r = (h * p) ^ <*(h . d)*>;
set i = (len p) + 1;
A1: len (h * (p ^ <*d*>)) = len (p ^ <*d*>) by FINSEQ_2:33;
A2: len (h * p) = len p by FINSEQ_2:33;
A3: len (p ^ <*d*>) = (len p) + 1 by FINSEQ_2:16;
then A4: dom (h * (p ^ <*d*>)) = Seg ((len p) + 1) by A1, FINSEQ_1:def 3;
reconsider p1 = p ^ <*d*> as FinSequence of D ;
A5: dom p1 = Seg ((len p) + 1) by A3, FINSEQ_1:def 3;
A6: for j being object st j in dom (h * (p ^ <*d*>)) holds
(h * p1) . j = ((h * p) ^ <*(h . d)*>) . j

proof

let j be object ; :: thesis: ( j in dom (h * (p ^ <*d*>)) implies (h * p1) . j = ((h * p) ^ <*(h . d)*>) . j )
A7: Seg (len p) = dom p by FINSEQ_1:def 3;
A8: Seg (len (h * p)) = dom (h * p) by FINSEQ_1:def 3;
assume A9: j in dom (h * (p ^ <*d*>)) ; :: thesis: (h * p1) . j = ((h * p) ^ <*(h . d)*>) . j

per cases then ( j in dom p or j = (len p) + 1 ) by A4, A7, FINSEQ_2:7;

suppose A10: j in dom p ; :: thesis: (h * p1) . j = ((h * p) ^ <*(h . d)*>) . j

(h * (p ^ <*d*>)) . j = h . (p1 . j) by A5, A4, A9, FUNCT_1:13
.= h . (p . j) by A10, FINSEQ_1:def 7
.= (h * p) . j by A2, A7, A8, A10, FUNCT_1:12
.= ((h * p) ^ <*(h . d)*>) . j by A2, A7, A8, A10, FINSEQ_1:def 7 ;
hence (h * p1) . j = ((h * p) ^ <*(h . d)*>) . j ; :: thesis: verum

end;

suppose A11: j = (len p) + 1 ; :: thesis: (h * p1) . j = ((h * p) ^ <*(h . d)*>) . j

(h * (p ^ <*d*>)) . j = h . (p1 . j) by A5, A4, A9, FUNCT_1:13
.= ((h * p) ^ <*(h . d)*>) . j by A2, A11 ;
hence (h * p1) . j = ((h * p) ^ <*(h . d)*>) . j ; :: thesis: verum

end;

end;

end;

len (h * (p ^ <*d*>)) = len (p ^ <*d*>) by FINSEQ_2:33
.= (len p) + 1 by FINSEQ_2:16
.= (len (h * p)) + 1 by FINSEQ_2:33
.= len ((h * p) ^ <*(h . d)*>) by FINSEQ_2:16 ;
hence h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> by A6, FINSEQ_3:29; :: thesis: verum