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