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] and
( ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;
( dom m = (m `1 ) `1 & cod m = (m `1 ) `2 & [A,B] = m `1 ) by A1, MCART_1:7;
then ( m `1 = [(dom m),(cod m)] & m `2 = m `2 ) by MCART_1:8;
hence m = [[(dom m),(cod m)],(m `2 )] by A1, MCART_1:8; :: thesis: verum