let X be non-empty 1 -element FinSequence; :: thesis: product X = { <*x*> where x is Element of X . 1 : verum }
A1: dom X = {1} by FINSEQ_1:89, FINSEQ_1:2;
A2: not X . 1 is empty

proof

assume A3: X . 1 is empty ; :: thesis: contradiction
1 in dom X by A1, TARSKI:def 1;
hence contradiction by A3; :: thesis: verum

end;

len X = 1 by CARD_1:def 7;
then X = <*(X . 1)*> by FINSEQ_1:40;
then consider I being Function of (X . 1),(product X) such that
I is one-to-one and
A4: I is onto and
A5: for x being object st x in X . 1 holds
I . x = <*x*> by A2, PRVECT_3:4;

now :: thesis: ( ( for t being object st t in product X holds
t in { <*x*> where x is Element of X . 1 : verum } ) & ( for t being object st t in { <*x*> where x is Element of X . 1 : verum } holds
t in product X ) )

hereby :: thesis: for t being object st t in { <*x*> where x is Element of X . 1 : verum } holds
t in product X

let t be object ; :: thesis: ( t in product X implies t in { <*x*> where x is Element of X . 1 : verum } )
assume t in product X ; :: thesis: t in { <*x*> where x is Element of X . 1 : verum }
then t in rng I by A4, FUNCT_2:def 3;
then consider a being object such that
A6: a in dom I and
A7: t = I . a by FUNCT_1:def 3;
t = <*a*> by A7, A6, A5;
hence t in { <*x*> where x is Element of X . 1 : verum } by A6; :: thesis: verum

end;

let t be object ; :: thesis: ( t in { <*x*> where x is Element of X . 1 : verum } implies t in product X )
assume t in { <*x*> where x is Element of X . 1 : verum } ; :: thesis: t in product X
then consider x being Element of X . 1 such that
A9: t = <*x*> ;
reconsider t1 = t as FinSequence by A9;
dom t1 = Seg 1 by A9, FINSEQ_1:def 8;
then A10: dom t1 = dom X by FINSEQ_1:89;
for a being object st a in dom X holds
t1 . a in X . a

proof

let a be object ; :: thesis: ( a in dom X implies t1 . a in X . a )
assume a in dom X ; :: thesis: t1 . a in X . a
then A11: a = 1 by A1, TARSKI:def 1;
then t1 . a is Element of X . 1 by A9;
hence t1 . a in X . a by A2, A11; :: thesis: verum

end;

hence t in product X by A10, CARD_3:def 5; :: thesis: verum

end;

then ( { <*x*> where x is Element of X . 1 : verum } c= product X & product X c= { <*x*> where x is Element of X . 1 : verum } ) ;
hence product X = { <*x*> where x is Element of X . 1 : verum } ; :: thesis: verum