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