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