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 A1: X in dom (.: ) ; :: thesis: (.: ) . X = R .: X
X in bool A by A1, Def3;
hence (.: ) . X = R .: X by Def3; :: thesis: verum