let B be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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:]; :: thesis: ( 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; :: thesis: ( ( 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) ; :: thesis: y in R .:^ X

per cases ( (.: R) .: {_{X}_} = {} or (.: R) .: {_{X}_} <> {} ) ;

suppose (.: R) .: {_{X}_} = {} ; :: thesis: y in R .:^ X

then Intersect ((.: R) .: {_{X}_}) = B by SETFAM_1:def 9;
hence y in R .:^ X ; :: thesis: verum

end;

suppose A2: (.: R) .: {_{X}_} <> {} ; :: thesis: y in R .:^ X

then A3: Intersect ((.: R) .: {_{X}_}) = meet ((.: R) .: {_{X}_}) by SETFAM_1:def 9;
for Y being set st Y in (.: R) .: {_{X}_} holds
y in Y

proof

let Y be set ; :: thesis: ( Y in (.: R) .: {_{X}_} implies y in Y )
assume Y in (.: R) .: {_{X}_} ; :: thesis: y in Y
then consider z being object such that
A4: [z,Y] in .: R and
A5: z in {_{X}_} by RELAT_1:def 13;
consider x being object such that
A6: z = {x} and
A7: x in X by A5, Th1;
A8: z in dom (.: R) by A4, FUNCT_1:1;
Y = (.: R) . z by A4, FUNCT_1:1;
then Y = Im (R,x) by A6, A8, Def1;
hence y in Y by A1, A7; :: thesis: verum

end;

hence y in R .:^ X by A2, A3, SETFAM_1:def 1; :: thesis: verum

end;

end;