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

now :: thesis: for x being object st x in rng (p ^ q) holds
x in (rng p) \/ (rng q)

let x be object ; :: thesis: ( x in rng (p ^ q) implies x in (rng p) \/ (rng q) )
assume x in rng (p ^ q) ; :: thesis: x in (rng p) \/ (rng q)
then consider y being object such that
A1: y in dom (p ^ q) and
A2: x = (p ^ q) . y by FUNCT_1:def 3;
A3: y in Seg ((len p) + (len q)) by A1, Def7;
reconsider k = y as Element of NAT by A1;
A4: 1 <= k by A3, Th1;
A5: k <= (len p) + (len q) by A3, Th1;

A6: now :: thesis: ( (len p) + 1 <= k implies x in rng q )

assume A7: (len p) + 1 <= k ; :: thesis: x in rng q
then A8: q . (k - (len p)) = x by A2, A5, Th23;
consider m being Nat such that
A9: ((len p) + 1) + m = k by A7, NAT_1:10;
(len p) + (1 + m) = k by A9;
then ( 1 + 0 <= 1 + m & 1 + m <= len q ) by A3, Th1, XREAL_1:6;
then 1 + m in Seg (len q) ;
then k - (len p) in dom q by A9, Def3;
hence x in rng q by A8, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: ( not (len p) + 1 <= k implies x in rng p )

assume not (len p) + 1 <= k ; :: thesis: x in rng p
then k <= len p by NAT_1:8;
then k in Seg (len p) by A4;
then A10: k in dom p by Def3;
then p . k = x by A2, Def7;
hence x in rng p by A10, FUNCT_1:def 3; :: thesis: verum

end;

hence x in (rng p) \/ (rng q) by A6, XBOOLE_0:def 3; :: thesis: verum

end;

then A11: rng (p ^ q) c= (rng p) \/ (rng q) ;
( rng p c= rng (p ^ q) & rng q c= rng (p ^ q) ) by Th29, Th30;
hence rng (p ^ q) = (rng p) \/ (rng q) by A11, XBOOLE_1:8; :: thesis: verum