let a, b be set ; :: 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

now

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;

then ( len p <= 1 & len p >= 0 + 1 ) by NAT_1:13;
hence a = b by A1, XXREAL_0:1; :: thesis: verum