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 ) ;
m = [[(dom m),(cod m)],(m `2 )] by Th8;
hence m = [[A,B],(m `2 )] by A1, ZFMISC_1:33; :: thesis: verum