theorem Th16: :: ENS_1:16

for V being non empty set
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)]