let V be non empty set ; :: thesis: for m being Element of Maps V holds m = [[(dom m),(cod m)],(m `2)]

let m be Element of Maps V; :: thesis: m = [[(dom m),(cod m)],(m `2)]

consider f being Element of Funcs V, A, B being Element of V such that

A1: ( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;

thus m = [[(dom m),(cod m)],(m `2)] by A1; :: thesis: verum

let m be Element of Maps V; :: thesis: m = [[(dom m),(cod m)],(m `2)]

consider f being Element of Funcs V, A, B being Element of V such that

A1: ( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;

thus m = [[(dom m),(cod m)],(m `2)] by A1; :: thesis: verum