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} * and
A2: y in {z} * and
A3: card x = card y ; :: thesis: x = y
reconsider x = x, y = y as FinSequence of {z} by A1, A2, FINSEQ_1:def 11;
A4: dom x = Seg (len x) by FINSEQ_1:def 3
.= dom y by A3, FINSEQ_1:def 3 ;
now :: thesis: for i being Nat st i in dom x holds
x . i = y . i
let i be Nat; :: thesis: ( i in dom x implies x . i = y . i )
assume A5: i in dom x ; :: thesis: x . i = y . i
then A6: x . i in rng x by FUNCT_1:def 3;
A7: y . i in rng y by A4, A5, FUNCT_1:def 3;
thus x . i = z by A6, TARSKI:def 1
.= y . i by A7, TARSKI:def 1 ; :: thesis: verum
end;
hence x = y by A4, FINSEQ_1:13; :: thesis: verum