let f be FinSequence; :: thesis: for g being XFinSequence holds
( rng (f ^ g) = (rng f) \/ (rng g) & rng (g ^ f) = (rng f) \/ (rng g) )
let g be XFinSequence; :: thesis: ( rng (f ^ g) = (rng f) \/ (rng g) & rng (g ^ f) = (rng f) \/ (rng g) )
A1: rng (f ^ g) c= (rng f) \/ (rng g)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f ^ g) or y in (rng f) \/ (rng g) )
assume y in rng (f ^ g) ; :: thesis: y in (rng f) \/ (rng g)
then consider x being object such that
B2: ( x in dom (f ^ g) & (f ^ g) . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by B2;
( y in rng f or y in rng g )

proof

per cases ( x in dom f or x - ((len f) + 1) in dom g ) by B2, FDX;

suppose C1: x in dom f ; :: thesis: ( y in rng f or y in rng g )

then f . x = y by Def2, B2;
hence ( y in rng f or y in rng g ) by C1, FUNCT_1:def 3; :: thesis: verum

end;

suppose C1: x - ((len f) + 1) in dom g ; :: thesis: ( y in rng f or y in rng g )

then g . (x - ((len f) + 1)) = (f ^ g) . (((x - ((len f) + 1)) + (len f)) + 1) by Def2
.= y by B2 ;
hence ( y in rng f or y in rng g ) by C1, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence y in (rng f) \/ (rng g) by XBOOLE_0:def 3; :: thesis: verum

end;

A2: (rng f) \/ (rng g) c= rng (f ^ g)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (rng f) \/ (rng g) or y in rng (f ^ g) )
assume y in (rng f) \/ (rng g) ; :: thesis: y in rng (f ^ g)

per cases then ( y in rng f or y in rng g ) by XBOOLE_0:def 3;

suppose y in rng f ; :: thesis: y in rng (f ^ g)

then consider x being object such that
C1: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by C1;
C2: x in dom (f ^ g) by C1, FDX;
(f ^ g) . x = y by C1, Def2;
hence y in rng (f ^ g) by C2, FUNCT_1:def 3; :: thesis: verum

end;

suppose y in rng g ; :: thesis: y in rng (f ^ g)

then consider x being object such that
C1: ( x in dom g & g . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by C1;
((x + (len f)) + 1) - ((len f) + 1) in dom g by C1;
then C2: (x + (len f)) + 1 in dom (f ^ g) by FDX;
(f ^ g) . (((len f) + x) + 1) = y by C1, Def2;
hence y in rng (f ^ g) by C2, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

A3: rng (g ^ f) c= (rng f) \/ (rng g)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (g ^ f) or y in (rng f) \/ (rng g) )
assume y in rng (g ^ f) ; :: thesis: y in (rng f) \/ (rng g)
then consider x being object such that
B2: ( x in dom (g ^ f) & (g ^ f) . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by B2;
( y in rng f or y in rng g )

proof

per cases ( x in dom g or (x + 1) - (len g) in dom f ) by B2, XDF;

suppose C1: x in dom g ; :: thesis: ( y in rng f or y in rng g )

then g . x = y by B2, Def1;
hence ( y in rng f or y in rng g ) by C1, FUNCT_1:def 3; :: thesis: verum

end;

suppose C1: (x + 1) - (len g) in dom f ; :: thesis: ( y in rng f or y in rng g )

then f . ((x + 1) - (len g)) = (g ^ f) . ((((x + 1) - (len g)) + (len g)) - 1) by Def1
.= y by B2 ;
hence ( y in rng f or y in rng g ) by C1, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence y in (rng f) \/ (rng g) by XBOOLE_0:def 3; :: thesis: verum

end;

(rng f) \/ (rng g) c= rng (g ^ f)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (rng f) \/ (rng g) or y in rng (g ^ f) )
assume y in (rng f) \/ (rng g) ; :: thesis: y in rng (g ^ f)

per cases then ( y in rng f or y in rng g ) by XBOOLE_0:def 3;

suppose y in rng f ; :: thesis: y in rng (g ^ f)

then consider x being object such that
C1: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by C1;
1 <= x by C1, FINSEQ_3:25;
then reconsider k = x - 1 as Nat ;
(((len g) + k) + 1) - (len g) in dom f by C1;
then C2: (len g) + k in dom (g ^ f) by XDF;
(g ^ f) . (((len g) + x) - 1) = y by C1, Def1;
hence y in rng (g ^ f) by C2, FUNCT_1:def 3; :: thesis: verum

end;

suppose y in rng g ; :: thesis: y in rng (g ^ f)

then consider x being object such that
C1: ( x in dom g & g . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by C1;
C2: x in dom (g ^ f) by C1, XDF;
(g ^ f) . x = y by C1, Def1;
hence y in rng (g ^ f) by C2, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence ( rng (f ^ g) = (rng f) \/ (rng g) & rng (g ^ f) = (rng f) \/ (rng g) ) by A1, A2, A3; :: thesis: verum