let i be natural Number ; 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 ; 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; 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; 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; 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; verum