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) & x = (p ^ q) . y ) by FUNCT_1:def 5;
A2: y in Seg ((len p) + (len q)) by A1, Def7;
reconsider k = y as Element of NAT by A1;
A3: ( 1 <= k & k <= (len p) + (len q) ) by A2, Th3;

A4: now

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

end;

hence x in (rng p) \/ (rng q) by A4, 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