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