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))

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

hence
h * ([#] (p,d)) = [#] ((h * p),(h . d))
by FUNCT_2:63; :: thesis: verumlet 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;

end;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

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