now :: thesis: ( p <> {} implies ex rr being FinSequence st rr = p * (Sgm ((dom p) \ (p " A))) )

assume p <> {} ; :: thesis: ex rr being FinSequence st rr = p * (Sgm ((dom p) \ (p " A)))
then reconsider D = Seg (len p) as non empty Subset of NAT ;
rng (Sgm ((Seg (len p)) \ (p " A))) = (Seg (len p)) \ (p " A) by FINSEQ_1:def 14;
then rng (Sgm ((Seg (len p)) \ (p " A))) c= D by XBOOLE_1:36;
then reconsider q = Sgm ((Seg (len p)) \ (p " A)) as FinSequence of D by FINSEQ_1:def 4;
reconsider r = p * q as FinSequence by FINSEQ_2:30;
take rr = r; :: thesis: rr = p * (Sgm ((dom p) \ (p " A)))
thus rr = p * (Sgm ((dom p) \ (p " A))) by FINSEQ_1:def 3; :: thesis: verum

end;

hence p * (Sgm ((dom p) \ (p " A))) is FinSequence ; :: thesis: verum