let V be non empty set ; :: thesis: for m, m9 being Element of Maps V st m `2 = m9 `2 & dom m = dom m9 & cod m = cod m9 holds
m = m9
let m, m9 be Element of Maps V; :: thesis: ( m `2 = m9 `2 & dom m = dom m9 & cod m = cod m9 implies m = m9 )
m = [[(dom m),(cod m)],(m `2)] by Th8;
hence ( m `2 = m9 `2 & dom m = dom m9 & cod m = cod m9 implies m = m9 ) by Th8; :: thesis: verum