let X be non empty set ; for x being Tuple of 4,X
for a, b, c, d being object st ( a = x . 1 or a = x . 2 or a = x . 3 or a = x . 4 ) & ( b = x . 1 or b = x . 2 or b = x . 3 or b = x . 4 ) & ( c = x . 1 or c = x . 2 or c = x . 3 or c = x . 4 ) & ( d = x . 1 or d = x . 2 or d = x . 3 or d = x . 4 ) holds
<*a,b,c,d*> is Tuple of 4,X
let x be Tuple of 4,X; for a, b, c, d being object st ( a = x . 1 or a = x . 2 or a = x . 3 or a = x . 4 ) & ( b = x . 1 or b = x . 2 or b = x . 3 or b = x . 4 ) & ( c = x . 1 or c = x . 2 or c = x . 3 or c = x . 4 ) & ( d = x . 1 or d = x . 2 or d = x . 3 or d = x . 4 ) holds
<*a,b,c,d*> is Tuple of 4,X
let a, b, c, d be object ; ( ( a = x . 1 or a = x . 2 or a = x . 3 or a = x . 4 ) & ( b = x . 1 or b = x . 2 or b = x . 3 or b = x . 4 ) & ( c = x . 1 or c = x . 2 or c = x . 3 or c = x . 4 ) & ( d = x . 1 or d = x . 2 or d = x . 3 or d = x . 4 ) implies <*a,b,c,d*> is Tuple of 4,X )
assume A1:
( ( a = x . 1 or a = x . 2 or a = x . 3 or a = x . 4 ) & ( b = x . 1 or b = x . 2 or b = x . 3 or b = x . 4 ) & ( c = x . 1 or c = x . 2 or c = x . 3 or c = x . 4 ) & ( d = x . 1 or d = x . 2 or d = x . 3 or d = x . 4 ) )
; <*a,b,c,d*> is Tuple of 4,X
set y = <*a,b,c,d*>;
dom x = Seg 4
by FINSEQ_2:124;
then A2:
( 1 in dom x & 2 in dom x & 3 in dom x & 4 in dom x )
;
reconsider d19 = <*a,b,c,d*> . 1, d29 = <*a,b,c,d*> . 2, d39 = <*a,b,c,d*> . 3, d49 = <*a,b,c,d*> . 4 as Element of X by A1, A2, FINSEQ_2:11;
( a is Element of X & b is Element of X & c is Element of X & d is Element of X )
by A1, A2, FINSEQ_2:11;
then
<*a,b,c,d*> in { <*d1,d2,d3,d4*> where d1, d2, d3, d4 is Element of X : verum }
;
then
<*a,b,c,d*> in 4 -tuples_on X
by Th02;
hence
<*a,b,c,d*> is Tuple of 4,X
by FINSEQ_2:131; verum