theorem
for
D,
D9,
E being non
empty set for
d1,
d2 being
Element of
D for
d19,
d29 being
Element of
D9 for
F being
Function of
[:D,D9:],
E for
p being
FinSequence of
D for
q being
FinSequence of
D9 st
p = <*d1,d2*> &
q = <*d19,d29*> holds
F .: (
p,
q)
= <*(F . (d1,d19)),(F . (d2,d29))*>