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