let x, y, z be set ; :: thesis: ( x in {z} * & y in {z} * & card x = card y implies x = y )
assume that
A1: ( x in {z} * & y in {z} * ) and
A2: card x = card y ; :: thesis: x = y
reconsider x = x, y = y as FinSequence of {z} by A1, FINSEQ_1:def 11;
A3: dom x = Seg (len x) by FINSEQ_1:def 3
.= dom y by A2, FINSEQ_1:def 3 ;

now

let i be Nat; :: thesis: ( i in dom x implies x . i = y . i )
assume i in dom x ; :: thesis: x . i = y . i
then A4: ( x . i in rng x & y . i in rng y & rng x c= {z} & rng y c= {z} ) by A3, FUNCT_1:def 5;
hence x . i = z by TARSKI:def 1
.= y . i by A4, TARSKI:def 1 ;
:: thesis: verum

end;

hence x = y by A3, FINSEQ_1:17; :: thesis: verum