let D, D9, E be non empty set ; :: thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D
for p9 being FinSequence of D9 holds
( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )
let F be Function of [:D,D9:],E; :: thesis: for p being FinSequence of D
for p9 being FinSequence of D9 holds
( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )
let p be FinSequence of D; :: thesis: for p9 being FinSequence of D9 holds
( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )
let p9 be FinSequence of D9; :: thesis: ( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )
reconsider r = F .: ((<*> D),p9), r9 = F .: (p,(<*> D9)) as FinSequence of E by Th68;
len (<*> D) = 0 ;
then ( len r = min (0,(len p9)) & len r9 = min ((len p),0) ) by Th69;
hence ( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E ) by XXREAL_0:def 9; :: thesis: verum