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

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