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

now

let x be set ; :: 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 set 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 (len p) + (len q) by A1, Def4;
then A3: k < (len p) + (len q) by NAT_1:44;

A4: now

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 len q by NAT_1:44;
q . (k - (len p)) = x by A2, A3, A5, Th21;
hence x in rng q by A6, A7, FUNCT_1:3; :: thesis: verum

end;

now

assume not len p <= k ; :: thesis: x in rng p
then A8: k in dom p by NAT_1:44;
then p . k = x by A2, Def4;
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) by TARSKI:def 3;
( rng p c= rng (p ^ q) & rng q c= rng (p ^ q) ) by Th27, Th28;
then (rng p) \/ (rng q) c= rng (p ^ q) by XBOOLE_1:8;
hence rng (p ^ q) = (rng p) \/ (rng q) by A9, XBOOLE_0:def 10; :: thesis: verum