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 ;
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 ;
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
.= ((h * p) ^ <*(h . d)*>) . j by ;
:: 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 ;
:: thesis: verum
end;
end;
end;
hence (h * (p ^ <*d*>)) . j = ((h * p) ^ <*(h . d)*>) . j by ; :: 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 ; :: thesis: verum