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) )

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

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

( cod m <> {} or dom m = {} )
by Th9;
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;then A2: m = [[A,B],(m `2)] by Th16;

thus ( dom m = A & cod m = B ) by A2; :: thesis: verum

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