let p, q be XFinSequence; :: thesis: rng p c= rng (p ^ q)

now

A1: dom p c= dom (p ^ q) by Th24;
let x be set ; :: thesis: ( x in rng p implies x in rng (p ^ q) )
assume x in rng p ; :: thesis: x in rng (p ^ q)
then consider y being set such that
A2: y in dom p and
A3: x = p . y by FUNCT_1:def 3;
reconsider k = y as Element of NAT by A2;
(p ^ q) . k = p . k by A2, Def4;
hence x in rng (p ^ q) by A2, A3, A1, FUNCT_1:3; :: thesis: verum

end;

hence rng p c= rng (p ^ q) by TARSKI:def 3; :: thesis: verum