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

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