let M be non empty set ; :: thesis: for X, Y being Element of M st X c= Y holds
(id M) . X c= (id M) . Y
let X, Y be Element of M; :: thesis: ( X c= Y implies (id M) . X c= (id M) . Y )
assume A1: X c= Y ; :: thesis: (id M) . X c= (id M) . Y
(id M) . X = X by FUNCT_1:18;
hence (id M) . X c= (id M) . Y by A1, FUNCT_1:18; :: thesis: verum