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