let p, q be FinSequence; :: 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 5;
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, Th3;
A5: k <= (len p) + (len q) by A3, Th3;

A6: now

assume A7: (len p) + 1 <= k ; :: thesis: x in rng q
then A8: q . (k - (len p)) = x by A2, A5, Th36;
consider m being Nat such that
A9: ((len p) + 1) + m = k by A7, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
(len p) + (1 + m) = k by A9;
then ( 1 + 0 <= 1 + m & 1 + m <= len q ) by A5, XREAL_1:8;
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 5; :: thesis: verum

end;

now

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 5; :: 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) by TARSKI:def 3;
( rng p c= rng (p ^ q) & rng q c= rng (p ^ q) ) by Th42, Th43;
then (rng p) \/ (rng q) c= rng (p ^ q) by XBOOLE_1:8;
hence rng (p ^ q) = (rng p) \/ (rng q) by A11, XBOOLE_0:def 10; :: thesis: verum