let X be set ; :: thesis: for A, B being set
for R being Subset of [:A,B:] st X in dom (.: ) holds
(.: ) . X = R .: X
let A, B be set ; :: thesis: for R being Subset of [:A,B:] st X in dom (.: ) holds
(.: ) . X = R .: X
let R be Subset of [:A,B:]; :: thesis: ( X in dom (.: ) implies (.: ) . X = R .: X )
assume X in dom (.: ) ; :: thesis: (.: ) . X = R .: X
then X in bool A by Def1;
hence (.: ) . X = R .: X by Def1; :: thesis: verum