let i be Nat; :: thesis: for D, D', E being non empty set
for F being Function of [:D,D':],E
for z1 being Tuple of i,D
for z2 being Tuple of i,D' holds F .: z1,z2 is Element of i -tuples_on E
let D, D', E be non empty set ; :: thesis: for F being Function of [:D,D':],E
for z1 being Tuple of i,D
for z2 being Tuple of i,D' holds F .: z1,z2 is Element of i -tuples_on E
let F be Function of [:D,D':],E; :: thesis: for z1 being Tuple of i,D
for z2 being Tuple of i,D' 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,D' holds F .: z1,z2 is Element of i -tuples_on E
let z2 be Tuple of i,D'; :: 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