let I be set ; :: thesis: for M being ManySortedSet of
for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
let M be ManySortedSet of ; :: thesis: for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive
let g, h be SetOp of M; :: thesis: ( g is reflexive & h is reflexive implies g * h is reflexive )
assume that
A1: g is reflexive and
A2: h is reflexive ; :: thesis: g * h is reflexive
let X be Element of Bool M; :: according to CLOSURE2:def 12 :: thesis: X c=' (g * h) . X
A3: dom h = Bool M by FUNCT_2:def 1;
A4: X c= h . X by A2, Def12;
h . X c= g . (h . X) by A1, Def12;
then X c= g . (h . X) by A4, PBOOLE:15;
hence X c=' (g * h) . X by A3, FUNCT_1:23; :: thesis: verum