let E, D 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

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:37;

now

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 Th22
.= (h * p) . i by A3, FUNCT_1:23
.= ([#] (h * p),(h . d)) . i by A2, A1, A3, Th22 ;
:: 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 Th22
.= ([#] (h * p),(h . d)) . i by A2, A1, A4, Th22 ;
:: thesis: verum

end;

end;

end;

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

end;

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