let C, D be non empty set ; :: thesis: for f being Function of C,D
for T being Element of 0 -tuples_on C holds f * T = <*> D
let f be Function of C,D; :: thesis: for T being Element of 0 -tuples_on C holds f * T = <*> D
let T be Element of 0 -tuples_on C; :: thesis: f * T = <*> D
T = <*> C by FINSEQ_2:113;
hence f * T = <*> D ; :: thesis: verum