let X be non-empty 1 -element FinSequence; :: thesis:
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:
1 in dom X by A1, TARSKI:def 1;
hence contradiction by A3; :: thesis:

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:

hereby :: thesis:

let t be object ; :: thesis:
assume t in product X ; :: thesis:
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:

end;

let t be object ; :: thesis:
assume t in { <*x*> where x is Element of X . 1 : verum } ; :: thesis:
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:
assume a in dom X ; :: thesis:
then A11: a = 1 by A1, TARSKI:def 1;
then t1 . a is Element of X . 1 by A9, FINSEQ_1:40;
hence t1 . a in X . a by A2, A11; :: thesis:

end;

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

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: