theorem Th7: :: MESFUNC3:7

for X being set
for F being FinSequence of X
for i being Nat st i in dom F holds
( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )