let p, q be FinSequence; :: thesis: rng q c= rng (p ^ q)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q or x in rng (p ^ q) )
assume x in rng q ; :: thesis: x in rng (p ^ q)
then consider y being object such that
A1: y in dom q and
A2: x = q . y by FUNCT_1:def 3;
reconsider k = y as Element of NAT by A1;
( (len p) + k in dom (p ^ q) & (p ^ q) . ((len p) + k) = q . k ) by A1, Def7, Th28;
hence x in rng (p ^ q) by A2, FUNCT_1:def 3; :: thesis: verum