let D, D9, E be non empty set ; :: thesis: for d9 being Element of D9

for F being Function of [:D,D9:],E

for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E

let d9 be Element of D9; :: thesis: for F being Function of [:D,D9:],E

for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E

let F be Function of [:D,D9:],E; :: thesis: for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E

let T be Tuple of 0 ,D; :: thesis: F [:] (T,d9) = <*> E

T = <*> D ;

hence F [:] (T,d9) = <*> E by FINSEQ_2:85; :: thesis: verum

for F being Function of [:D,D9:],E

for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E

let d9 be Element of D9; :: thesis: for F being Function of [:D,D9:],E

for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E

let F be Function of [:D,D9:],E; :: thesis: for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E

let T be Tuple of 0 ,D; :: thesis: F [:] (T,d9) = <*> E

T = <*> D ;

hence F [:] (T,d9) = <*> E by FINSEQ_2:85; :: thesis: verum