let i be natural Number ; :: thesis: for D, D9, E being non empty set
for F being Function of [:D,D9:],E
for z1 being Tuple of i,D
for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E
let D, D9, E be non empty set ; :: thesis: for F being Function of [:D,D9:],E
for z1 being Tuple of i,D
for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E
let F be Function of [:D,D9:],E; :: thesis: for z1 being Tuple of i,D
for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E
let z1 be Tuple of i,D; :: thesis: for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E
let z2 be Tuple of i,D9; :: thesis: F .: (z1,z2) is Element of i -tuples_on E
reconsider r = F .: (z1,z2) as FinSequence of E by Th68;
( len z1 = i & len z2 = i ) by CARD_1:def 7;
then len r = i by Th70;
hence F .: (z1,z2) is Element of i -tuples_on E by Th90; :: thesis: verum