theorem Th17: :: FIN_TOPO:17

for FT being non empty RelStr
for A being Subset of FT holds ((A `) ^b) ` = A ^i