let r1, r2 be continuous Function of X,X0; :: thesis: ( r1 is being_a_retraction & r2 is being_a_retraction implies r1 = r2 )
assume A1: ( r1 is being_a_retraction & r2 is being_a_retraction ) ; :: thesis: r1 = r2
reconsider M = the carrier of X0 as non empty Subset of X by TSEP_1:1;
for x being set st x in the carrier of X holds
r1 . x = r2 . x

proof

let x be set ; :: 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 ;
( M /\ (MaxADSet a) = {(r1 . a)} & M /\ (MaxADSet a) = {(r2 . a)} ) by A1, Lm3;
hence r1 . x = r2 . x by ZFMISC_1:6; :: thesis: verum

end;

hence r1 = r2 by FUNCT_2:18; :: thesis: verum