let D, D9, E be non empty set ; :: thesis: for i being natural Number
for F being Function of [:D,D9:],E
for T9 being Tuple of i,D9
for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E
let i be natural Number ; :: thesis: for F being Function of [:D,D9:],E
for T9 being Tuple of i,D9
for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E
let F be Function of [:D,D9:],E; :: thesis: for T9 being Tuple of i,D9
for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E
let T9 be Tuple of i,D9; :: thesis: for T being Tuple of 0 ,D holds F .: (T,T9) = <*> E
let T be Tuple of 0 ,D; :: thesis: F .: (T,T9) = <*> E
T = <*> D ;
hence F .: (T,T9) = <*> E by FINSEQ_2:73; :: thesis: verum