let V be non empty set ; :: thesis: for A, B being Element of V

for m being Element of Maps V st m in Maps (A,B) holds

m = [[A,B],(m `2)]

let A, B be Element of V; :: thesis: for m being Element of Maps V st m in Maps (A,B) holds

m = [[A,B],(m `2)]

let m be Element of Maps V; :: thesis: ( m in Maps (A,B) implies m = [[A,B],(m `2)] )

assume m in Maps (A,B) ; :: thesis: m = [[A,B],(m `2)]

then A1: ex f being Element of Funcs V st

( m = [[A,B],f] & [[A,B],f] in Maps V ) ;

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

for m being Element of Maps V st m in Maps (A,B) holds

m = [[A,B],(m `2)]

let A, B be Element of V; :: thesis: for m being Element of Maps V st m in Maps (A,B) holds

m = [[A,B],(m `2)]

let m be Element of Maps V; :: thesis: ( m in Maps (A,B) implies m = [[A,B],(m `2)] )

assume m in Maps (A,B) ; :: thesis: m = [[A,B],(m `2)]

then A1: ex f being Element of Funcs V st

( m = [[A,B],f] & [[A,B],f] in Maps V ) ;

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