theorem Th7: :: FUNCOP_1:7

for A being set
for x, z being object st x in A holds
(A --> z) . x = z