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 Element of 0 -tuples_on D' holds F [;] d,T' = <*> E
let d be Element of D; :: thesis: for F being Function of [:D,D':],E
for T' being Element of 0 -tuples_on D' holds F [;] d,T' = <*> E
let F be Function of [:D,D':],E; :: thesis: for T' being Element of 0 -tuples_on D' holds F [;] d,T' = <*> E
let T' be Element of 0 -tuples_on D'; :: thesis: F [;] d,T' = <*> E
T' = <*> D' by FINSEQ_2:113;
hence F [;] d,T' = <*> E by FINSEQ_2:93; :: thesis: verum