let D, D9, E be non empty set ; 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; 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; for T being Tuple of 0 ,D holds F [:] (T,d9) = <*> E
let T be Tuple of 0 ,D; F [:] (T,d9) = <*> E
T = <*> D
;
hence
F [:] (T,d9) = <*> E
by FINSEQ_2:85; verum