reconsider M = the carrier of X0 as non empty Subset of X by TSEP_1:1;
let r1, r2 be continuous Function of X,X0; :: thesis: ( r1 is being_a_retraction & r2 is being_a_retraction implies r1 = r2 )
assume that
A1: r1 is being_a_retraction and
A2: r2 is being_a_retraction ; :: thesis: r1 = r2
for x being object st x in the carrier of X holds
r1 . x = r2 . x
proof
let x be object ; :: thesis: ( x in the carrier of X implies r1 . x = r2 . x )
assume x in the carrier of X ; :: thesis: r1 . x = r2 . x
then reconsider a = x as Point of X ;
A3: M /\ (MaxADSet a) = {(r2 . a)} by A2, Lm3;
M /\ (MaxADSet a) = {(r1 . a)} by A1, Lm3;
hence r1 . x = r2 . x by A3, ZFMISC_1:3; :: thesis: verum
end;
hence r1 = r2 by FUNCT_2:12; :: thesis: verum