let a, b be object ; :: thesis: ( {} reduces a,b implies a = b )
given p being RedSequence of {} such that A1: ( p . 1 = a & p . (len p) = b ) ; :: according to REWRITE1:def 3 :: thesis: a = b

A2: now :: thesis: not len p > 1

assume len p > 1 ; :: thesis: contradiction
then ( 1 in dom p & 1 + 1 in dom p ) by Lm3, Lm4;
hence contradiction by Def2; :: thesis: verum

end;

len p >= 0 + 1 by NAT_1:13;
hence a = b by A1, A2, XXREAL_0:1; :: thesis: verum