let a be FinSequence; :: thesis: {a} is relation-like
thus for z being set st z in {a} holds
z is FinSequence by TARSKI:def 1; :: according to MARGREL1:def 1 :: thesis: for a, b being FinSequence st a in {a} & b in {a} holds
len a = len b
thus for a1, a2 being FinSequence st a1 in {a} & a2 in {a} holds
len a1 = len a2 :: thesis: verum

proof

let a1, a2 be FinSequence; :: thesis: ( a1 in {a} & a2 in {a} implies len a1 = len a2 )
assume ( a1 in {a} & a2 in {a} ) ; :: thesis: len a1 = len a2
then ( a1 = a & a2 = a ) by TARSKI:def 1;
hence len a1 = len a2 ; :: thesis: verum

end;