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

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