let X be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( ( 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 ) ) ; :: thesis: <*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; :: thesis: verum