let B be non empty set ; for A being set
for X being Subset of A
for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
let A be set ; for X being Subset of A
for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
let X be Subset of A; for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
let y be Element of B; for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
let R be Subset of [:A,B:]; ( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
thus
( y in R .:^ X implies for x being set st x in X holds
y in Im (R,x) )
by Th24; ( ( for x being set st x in X holds
y in Im (R,x) ) implies y in R .:^ X )
assume A1:
for x being set st x in X holds
y in Im (R,x)
; y in R .:^ X