let S1, S2 be Sequence; :: thesis: ( rng S1 c= rng (S1 ^ S2) & rng S2 c= rng (S1 ^ S2) )
set q = S1 ^ S2;
A1: dom (S1 ^ S2) = (dom S1) +^ (dom S2) by ORDINAL4:def 1;
then A2: dom S1 c= dom (S1 ^ S2) by ORDINAL3:24;
thus rng S1 c= rng (S1 ^ S2) :: thesis: rng S2 c= rng (S1 ^ S2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng S1 or x in rng (S1 ^ S2) )
assume x in rng S1 ; :: thesis: x in rng (S1 ^ S2)
then consider z being object such that
A3: ( z in dom S1 & x = S1 . z ) by FUNCT_1:def 3;
reconsider z = z as Ordinal by A3;
( (S1 ^ S2) . z = x & z in dom (S1 ^ S2) ) by A3, A2, ORDINAL4:def 1;
hence x in rng (S1 ^ S2) by FUNCT_1:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng S2 or x in rng (S1 ^ S2) )
assume x in rng S2 ; :: thesis: x in rng (S1 ^ S2)
then consider z being object such that
A4: ( z in dom S2 & x = S2 . z ) by FUNCT_1:def 3;
reconsider z = z as Ordinal by A4;
( (S1 ^ S2) . ((dom S1) +^ z) = x & (dom S1) +^ z in dom (S1 ^ S2) ) by A1, A4, ORDINAL3:17, ORDINAL4:def 1;
hence x in rng (S1 ^ S2) by FUNCT_1:def 3; :: thesis: verum