let D be non empty set ; :: thesis: for x1, x2, x3, x4, x5, x6, x7, x8 being Element of 4 -tuples_on D holds <*(x1 ^ x5),(x2 ^ x6),(x3 ^ x7),(x4 ^ x8)*> is Element of 4 -tuples_on (8 -tuples_on D)
let x1, x2, x3, x4, x5, x6, x7, x8 be Element of 4 -tuples_on D; :: thesis: <*(x1 ^ x5),(x2 ^ x6),(x3 ^ x7),(x4 ^ x8)*> is Element of 4 -tuples_on (8 -tuples_on D)
X1: D c= D ;
then P1: x1 ^ x5 is Element of 8 -tuples_on D by FINSEQ_2:109;
P2: x2 ^ x6 is Element of 8 -tuples_on D by X1, FINSEQ_2:109;
P3: x3 ^ x7 is Element of 8 -tuples_on D by X1, FINSEQ_2:109;
x4 ^ x8 is Element of 8 -tuples_on D by X1, FINSEQ_2:109;
hence <*(x1 ^ x5),(x2 ^ x6),(x3 ^ x7),(x4 ^ x8)*> is Element of 4 -tuples_on (8 -tuples_on D) by P1, P2, P3, LMGSEQ4; :: thesis: verum