let X, Y be set ; for x being object st x in X holds
Im ([:X,Y:],x) = Y
let x be object ; ( x in X implies Im ([:X,Y:],x) = Y )
assume A1:
x in X
; Im ([:X,Y:],x) = Y
thus
Im ([:X,Y:],x) c= Y
XBOOLE_0:def 10 Y c= Im ([:X,Y:],x)
let y be object ; TARSKI:def 3 ( not y in Y or y in Im ([:X,Y:],x) )
assume
y in Y
; y in Im ([:X,Y:],x)
then A2:
[x,y] in [:X,Y:]
by A1, ZFMISC_1:87;
x in {x}
by TARSKI:def 1;
hence
y in Im ([:X,Y:],x)
by A2, Def11; verum