let p, q be XFinSequence; :: 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;
reconsider k = y as Element of NAT by A1;
y in Segm ((len p) + (len q)) by A1, Def3;
then A3: k < (len p) + (len q) by NAT_1:44;

A4: now :: thesis: ( len p <= k implies x in rng q )

assume A5: len p <= k ; :: thesis: x in rng q
then consider m being Nat such that
A6: (len p) + m = k by NAT_1:10;
(m + (len p)) - (len p) < ((len p) + (len q)) - (len p) by A3, A6, XREAL_1:14;
then A7: m in Segm (len q) by Lm1;
q . (k - (len p)) = x by A2, A3, A5, Th16;
hence x in rng q by A6, A7, FUNCT_1:3; :: thesis: verum

end;

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

assume not len p <= k ; :: thesis: x in rng p
then A8: k in dom p by Lm1;
then p . k = x by A2, Def3;
hence x in rng p by A8, FUNCT_1:3; :: thesis: verum

end;

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

end;

then A9: rng (p ^ q) c= (rng p) \/ (rng q) ;
( rng p c= rng (p ^ q) & rng q c= rng (p ^ q) ) by Th22, Th23;
then (rng p) \/ (rng q) c= rng (p ^ q) by XBOOLE_1:8;
hence rng (p ^ q) = (rng p) \/ (rng q) by A9; :: thesis: verum