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:37;
A2: len (p ^ <*d*>) = (len p) + 1 by FINSEQ_2:19;
A3: len ((h * p) ^ <*(h . d)*>) = (len (h * p)) + 1 by FINSEQ_2:19;
A4: len (h * p) = len p by FINSEQ_2:37;
X: dom (h * (p ^ <*d*>)) = Seg ((len p) + 1) by A1, A2, FINSEQ_1:def 3;

now

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

now

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

suppose A9: 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 A4, A7, A8, A9, FUNCT_1:22
.= ((h * p) ^ <*(h . d)*>) . j by A4, A7, A8, A9, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

hence h . ((p ^ <*d*>) . j) = h . d by FINSEQ_1:59
.= ((h * p) ^ <*(h . d)*>) . j by A4, A10, FINSEQ_1:59 ;
:: thesis: verum

end;

end;

end;

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

end;

hence h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*> by A1, A2, A3, A4, FINSEQ_2:10; :: thesis: verum