let V be non empty set ; :: thesis: for m being Element of Maps V holds

( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) )

let m be Element of Maps V; :: thesis: ( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) )

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

A1: m = [[A,B],f] and

A2: ( ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;

thus ( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) ) by A1, A2; :: thesis: verum

( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) )

let m be Element of Maps V; :: thesis: ( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) )

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

A1: m = [[A,B],f] and

A2: ( ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;

thus ( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) ) by A1, A2; :: thesis: verum