let D, E be non empty set ; :: thesis: for d being Element of D
for p being FinSequence of D
for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
let d be Element of D; :: thesis: for p being FinSequence of D
for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
let p be FinSequence of D; :: thesis: for h being Function of D,E holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>
let h be Function of D,E; :: 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;
len (p ^ <*d*>) = (len p) + 1 by FINSEQ_2:16;
then A3: dom (h * (p ^ <*d*>)) = Seg ((len p) + 1) by A1, FINSEQ_1:def 3;

A4: now :: thesis: for j being Nat st j in dom (h * (p ^ <*d*>)) holds
(h * (p ^ <*d*>)) . j = ((h * p) ^ <*(h . d)*>) . j

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

now :: thesis: h . ((p ^ <*d*>) . j) = ((h * p) ^ <*(h . d)*>) . j

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

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

hence h . ((p ^ <*d*>) . j) = h . (p . j) by FINSEQ_1:def 7
.= (h * p) . j by A2, A5, A6, A8, FUNCT_1:12
.= ((h * p) ^ <*(h . d)*>) . j by A2, A5, A6, A8, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

hence h . ((p ^ <*d*>) . j) = h . d by FINSEQ_1:42
.= ((h * p) ^ <*(h . d)*>) . j by A2, A9, FINSEQ_1:42 ;
:: thesis: verum

end;

end;

end;

hence (h * (p ^ <*d*>)) . j = ((h * p) ^ <*(h . d)*>) . j by A7, FUNCT_1:12; :: thesis: verum

end;

len ((h * p) ^ <*(h . d)*>) = (len (h * p)) + 1 by FINSEQ_2:16;
hence h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> by A1, A2, A4, FINSEQ_2:9, FINSEQ_2:16; :: thesis: verum