let D', D, E be non empty set ; :: thesis: for i being Nat
for F being Function of [:D,D':],E
for T' being Tuple of ,D'
for T being Tuple of ,D holds F .: T,T' = <*> E
let i be Nat; :: thesis: for F being Function of [:D,D':],E
for T' being Tuple of ,D'
for T being Tuple of ,D holds F .: T,T' = <*> E
let F be Function of [:D,D':],E; :: thesis: for T' being Tuple of ,D'
for T being Tuple of ,D holds F .: T,T' = <*> E
let T' be Tuple of ,D'; :: thesis: for T being Tuple of ,D holds F .: T,T' = <*> E
let T be Tuple of ,D; :: thesis: F .: T,T' = <*> E
T = <*> D ;
hence F .: T,T' = <*> E by FINSEQ_2:87; :: thesis: verum