let V be non empty set ; :: thesis: for A, B being Element of V
for m being Element of Maps V holds
( m in Maps (A,B) iff ( dom m = A & cod m = B ) )
let A, B be Element of V; :: thesis: for m being Element of Maps V holds
( m in Maps (A,B) iff ( dom m = A & cod m = B ) )
let m be Element of Maps V; :: thesis: ( m in Maps (A,B) iff ( dom m = A & cod m = B ) )
A1: m `2 is Function of (dom m),(cod m) by Th9;
thus ( m in Maps (A,B) implies ( dom m = A & cod m = B ) ) :: thesis: ( dom m = A & cod m = B implies m in Maps (A,B) )

proof

assume m in Maps (A,B) ; :: thesis: ( dom m = A & cod m = B )
then A2: m = [[A,B],(m `2)] by Th16;
thus ( dom m = A & cod m = B ) by A2; :: thesis: verum

end;

( cod m <> {} or dom m = {} ) by Th9;
then [[(dom m),(cod m)],(m `2)] in Maps ((dom m),(cod m)) by A1, Th15;
hence ( dom m = A & cod m = B implies m in Maps (A,B) ) by Th8; :: thesis: verum