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