let D, E be non empty set ; :: thesis: for d being Element of D
for h being Function of D,E
for p being FinSequence of D holds h * ([#] (p,d)) = [#] ((h * p),(h . d))
let d be Element of D; :: thesis: for h being Function of D,E
for p being FinSequence of D holds h * ([#] (p,d)) = [#] ((h * p),(h . d))
let h be Function of D,E; :: thesis: for p being FinSequence of D holds h * ([#] (p,d)) = [#] ((h * p),(h . d))
let p be FinSequence of D; :: thesis: h * ([#] (p,d)) = [#] ((h * p),(h . d))

now :: thesis: for i being Element of NAT holds (h * ([#] (p,d))) . i = ([#] ((h * p),(h . d))) . i

let i be Element of NAT ; :: thesis: (h * ([#] (p,d))) . i = ([#] ((h * p),(h . d))) . i
A1: dom (h * p) = Seg (len (h * p)) by FINSEQ_1:def 3;
A2: ( len (h * p) = len p & Seg (len p) = dom p ) by FINSEQ_1:def 3, FINSEQ_2:33;

now :: thesis: h . (([#] (p,d)) . i) = ([#] ((h * p),(h . d))) . i

per cases ( i in dom p or not i in dom p ) ;

suppose A3: i in dom p ; :: thesis: h . (([#] (p,d)) . i) = ([#] ((h * p),(h . d))) . i

hence h . (([#] (p,d)) . i) = h . (p . i) by Th20
.= (h * p) . i by A3, FUNCT_1:13
.= ([#] ((h * p),(h . d))) . i by A2, A1, A3, Th20 ;
:: thesis: verum

end;

suppose A4: not i in dom p ; :: thesis: h . (([#] (p,d)) . i) = ([#] ((h * p),(h . d))) . i

hence h . (([#] (p,d)) . i) = h . d by Th20
.= ([#] ((h * p),(h . d))) . i by A2, A1, A4, Th20 ;
:: thesis: verum

end;

end;

end;

hence (h * ([#] (p,d))) . i = ([#] ((h * p),(h . d))) . i by FUNCT_2:15; :: thesis: verum

end;

hence h * ([#] (p,d)) = [#] ((h * p),(h . d)) by FUNCT_2:63; :: thesis: verum