let h1, h2 be Function of (TOL X),(MapsT X); :: thesis: ( ( for T being Element of TOL X holds h1 . T = id$ T ) & ( for T being Element of TOL X holds h2 . T = id$ T ) implies h1 = h2 )
assume that
A19: for T being Element of TOL X holds h1 . T = id$ T and
A20: for T being Element of TOL X holds h2 . T = id$ T ; :: thesis: h1 = h2

now

let T be Element of TOL X; :: thesis: h1 . T = h2 . T
thus h1 . T = id$ T by A19
.= h2 . T by A20 ; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:113; :: thesis: verum