theorem Th112: :: FINSEQ_3:114

for A being set
for F being FinSequence holds (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of (dom F)