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 A1: ( g1 = f1 || S & g2 = f2 || S ) ; :: thesis: ( not f1 absorbs f2 or g1 absorbs g2 )
assume A2: 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
A3: ( dom g1 = [:S,S:] & dom g2 = [:S,S:] ) by FUNCT_2:def 1;
hence g1 . a,(g2 . a,b) = f1 . [a,(g2 . a,b)] by A1, FUNCT_1:70
.= f1 . [a,(f2 . [a,b])] by A1, A3, FUNCT_1:70
.= f1 . a,(f2 . a,b)
.= a by A2 ;
:: thesis: verum