let D be non empty set ; :: thesis: 3 -tuples_on D = { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }
now let x be
set ;
:: thesis: ( ( x in 3 -tuples_on D implies x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } ) & ( x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } implies x in 3 -tuples_on D ) )thus
(
x in 3
-tuples_on D implies
x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } )
:: thesis: ( x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } implies x in 3 -tuples_on D )proof
assume
x in 3
-tuples_on D
;
:: thesis: x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }
then consider s being
Element of
D * such that A1:
x = s
and A2:
len s = 3
;
( 1
in Seg 3 & 2
in Seg 3 & 3
in Seg 3 )
;
then
( 1
in dom s & 2
in dom s & 3
in dom s )
by A2, FINSEQ_1:def 3;
then reconsider d1' =
s . 1,
d2' =
s . 2,
d3' =
s . 3 as
Element of
D by Th13;
s = <*d1',d2',d3'*>
by A2, FINSEQ_1:62;
hence
x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }
by A1;
:: thesis: verum
end; assume
x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }
;
:: thesis: x in 3 -tuples_on Dthen consider d1,
d2,
d3 being
Element of
D such that A3:
x = <*d1,d2,d3*>
;
<*d1,d2,d3*> is
FinSequence of
D
by Th16;
then
(
len <*d1,d2,d3*> = 3 &
<*d1,d2,d3*> is
Element of
D * )
by FINSEQ_1:62, FINSEQ_1:def 11;
hence
x in 3
-tuples_on D
by A3;
:: thesis: verum end;
hence
3 -tuples_on D = { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }
by TARSKI:2; :: thesis: verum