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

now

let x be set ; :: thesis: ( x in rng q implies x in rng (p ^ q) )
assume x in rng q ; :: thesis: x in rng (p ^ q)
then consider y being set such that
A1: ( y in dom q & x = q . y ) by FUNCT_1:def 5;
reconsider k = y as Element of NAT by A1;
A2: (len p) + k in dom (p ^ q) by A1, Th41;
(p ^ q) . ((len p) + k) = q . k by A1, Def7;
hence x in rng (p ^ q) by A1, A2, FUNCT_1:def 5; :: thesis: verum

end;

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