let a be FinSequence; :: thesis: {a} is relation
for z being set st z in {a} holds
z is FinSequence by TARSKI:def 1;
then reconsider X = {a} as FinSequence-membered set by FINSEQ_1:def 19;
X is with_common_domain

proof

let a1 be FinSequence; :: according to MARGREL1:def 1 :: thesis: for b being FinSequence st a1 in X & b in X holds
len a1 = len b
let a2 be FinSequence; :: thesis: ( a1 in X & a2 in X implies len a1 = len a2 )
assume that
A1: a1 in X and
A2: a2 in X ; :: thesis: len a1 = len a2
a1 = a by A1, TARSKI:def 1;
hence len a1 = len a2 by A2, TARSKI:def 1; :: thesis: verum

end;

hence {a} is relation ; :: thesis: verum