let X be set ; :: thesis: for m, m1 being Element of MapsT X st m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 holds
m = m1
let m, m1 be Element of MapsT X; :: thesis: ( m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 implies m = m1 )
m = [[(dom m),(cod m)],(m `2)] by Th41;
hence ( m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 implies m = m1 ) by Th41; :: thesis: verum