let A, B be set ; :: thesis: for X being Subset of A
for R being Subset of [:A,B:] st X = {} holds
R .:^ X = B
let X be Subset of A; :: thesis: for R being Subset of [:A,B:] st X = {} holds
R .:^ X = B
let R be Subset of [:A,B:]; :: 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