let A, B be Sequence; :: thesis: rng A c= rng (A ^ B)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng A or y in rng (A ^ B) )
assume y in rng A ; :: thesis: y in rng (A ^ B)
then consider x being object such that
A1: ( x in dom A & A . x = y ) by FUNCT_1:def 3;
A2: (A ^ B) . x = y by A1, Def1;
dom A c= (dom A) +^ (dom B) by ORDINAL3:24;
then dom A c= dom (A ^ B) by Def1;
hence y in rng (A ^ B) by A1, A2, FUNCT_1:3; :: thesis: verum