let A, B be set ; :: thesis: for X being Subset of
for R being Subset of st X = {} holds
R .:^ X = B
let X be Subset of ; :: thesis: for R being Subset of st X = {} holds
R .:^ X = B
let R be Subset of ; :: thesis: ( X = {} implies R .:^ X = B )
assume X = {} ; :: thesis: R .:^ X = B
then (.: R) .: {_{X}_} = {} by Th23;
hence R .:^ X = B by SETFAM_1:def 10; :: thesis: verum