let D be non empty set ; :: thesis: for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2
let S be non empty Subset of D; :: thesis: for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2
let f1, f2 be BinOp of D; :: thesis: for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2
let g1, g2 be BinOp of S; :: thesis: ( g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 implies g1 absorbs g2 )
assume that
A1: g1 = f1 || S and
A2: g2 = f2 || S ; :: thesis: ( not f1 absorbs f2 or g1 absorbs g2 )
assume A3: for a, b being Element of D holds f1 . (a,(f2 . (a,b))) = a ; :: according to LATTICE2:def 1 :: thesis: g1 absorbs g2
let a, b be Element of S; :: according to LATTICE2:def 1 :: thesis: g1 . (a,(g2 . (a,b))) = a
A4: dom g2 = [:S,S:] by FUNCT_2:def 1;
dom g1 = [:S,S:] by FUNCT_2:def 1;
hence g1 . (a,(g2 . (a,b))) = f1 . [a,(g2 . (a,b))] by A1, FUNCT_1:47
.= f1 . [a,(f2 . [a,b])] by A2, A4, FUNCT_1:47
.= f1 . (a,(f2 . (a,b)))
.= a by A3 ;
:: thesis: verum