let i be Nat; :: 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 Th84;
( len z1 = i & len z2 = i ) by FINSEQ_1:def 18;
then len r = i by Th86;
hence F .: z1,z2 is Element of i -tuples_on E by Th110; :: thesis: verum