let i be Nat; :: thesis: for D, D', E being non empty set
for F being Function of [:D,D':],E
for z1 being Element of i -tuples_on D
for z2 being Element of i -tuples_on 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 Element of i -tuples_on D
for z2 being Element of i -tuples_on D' holds F .: z1,z2 is Element of i -tuples_on E
let F be Function of [:D,D':],E; :: thesis: for z1 being Element of i -tuples_on D
for z2 being Element of i -tuples_on D' holds F .: z1,z2 is Element of i -tuples_on E
let z1 be Element of i -tuples_on D; :: thesis: for z2 being Element of i -tuples_on D' holds F .: z1,z2 is Element of i -tuples_on E
let z2 be Element of i -tuples_on 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 Th109;
then len r = i by Th86;
hence F .: z1,z2 is Element of i -tuples_on E by Th110; :: thesis: verum