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

proof

let x be set ; :: 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 set such that
A1: ( z in dom S1 & x = S1 . z ) by FUNCT_1:def 5;
reconsider z = z as Ordinal by A1;
( (S1 ^ S2) . z = x & z in dom (S1 ^ S2) ) by A1, A2, ORDINAL4:def 1;
hence x in rng (S1 ^ S2) by FUNCT_1:def 5; :: thesis: verum

end;

let x be set ; :: 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 set such that
A1: ( z in dom S2 & x = S2 . z ) by FUNCT_1:def 5;
reconsider z = z as Ordinal by A1;
( (S1 ^ S2) . ((dom S1) +^ z) = x & (dom S1) +^ z in dom (S1 ^ S2) ) by A0, A1, ORDINAL4:def 1, ORDINAL3:20;
hence x in rng (S1 ^ S2) by FUNCT_1:def 5; :: thesis: verum