let A, B be set ; :: thesis: for y being set st A meets rng ((id B) +* (A --> y)) holds
y in A
let y be set ; :: thesis: ( A meets rng ((id B) +* (A --> y)) implies y in A )
assume A meets rng ((id B) +* (A --> y)) ; :: thesis: y in A
then consider x being object such that
A1: x in A and
A2: x in rng ((id B) +* (A --> y)) by XBOOLE_0:3;
consider z being object such that
A3: z in dom ((id B) +* (A --> y)) and
A4: ((id B) +* (A --> y)) . z = x by A2, FUNCT_1:def 3;
A5: z in (dom (id B)) \/ (dom (A --> y)) by A3, FUNCT_4:def 1;

per cases ( z in dom (A --> y) or not z in dom (A --> y) ) ;

suppose A6: z in dom (A --> y) ; :: thesis: y in A

then y = (A --> y) . z by FUNCOP_1:7
.= x by A4, A6, FUNCT_4:13 ;
hence y in A by A1; :: thesis: verum

end;

suppose A7: not z in dom (A --> y) ; :: thesis: y in A

then A8: z in dom (id B) by A5, XBOOLE_0:def 3;
x = (id B) . z by A4, A7, FUNCT_4:11
.= z by A8, FUNCT_1:18 ;
hence y in A by A1, A7; :: thesis: verum

end;

end;