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 Th84;
len (<*> D) = 0 ;
then ( len r = min 0 ,(len p9) & len r9 = min (len p),0 ) by Th85;
hence ( F .: (<*> D),p9 = <*> E & F .: p,(<*> D9) = <*> E ) by XXREAL_0:def 9; :: thesis: verum