let D1, D2 be non empty set ; :: thesis: for f1, g1 being BinOp of D1

for f2, g2 being BinOp of D2 holds

( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )

let f1, g1 be BinOp of D1; :: thesis: for f2, g2 being BinOp of D2 holds

( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )

let f2, g2 be BinOp of D2; :: thesis: ( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )

defpred S_{1}[ set , set ] means |:f1,f2:| . ($1,(|:g1,g2:| . ($1,$2))) = $1;

thus ( f1 absorbs g1 & f2 absorbs g2 implies |:f1,f2:| absorbs |:g1,g2:| ) :: thesis: ( |:f1,f2:| absorbs |:g1,g2:| implies ( f1 absorbs g1 & f2 absorbs g2 ) )

thus for a1, b1 being Element of D1 holds f1 . (a1,(g1 . (a1,b1))) = a1 :: according to LATTICE2:def 1 :: thesis: f2 absorbs g2

let a2 be Element of D2; :: according to LATTICE2:def 1 :: thesis: for b_{1} being Element of D2 holds f2 . (a2,(g2 . (a2,b_{1}))) = a2

let b2 be Element of D2; :: thesis: f2 . (a2,(g2 . (a2,b2))) = a2

[ the Element of D1,a2] = |:f1,f2:| . ([ the Element of D1,a2],(|:g1,g2:| . ([ the Element of D1,a2],[ the Element of D1,b2]))) by A4

.= |:f1,f2:| . ([ the Element of D1,a2],[(g1 . ( the Element of D1, the Element of D1)),(g2 . (a2,b2))]) by Th21

.= [(f1 . ( the Element of D1,(g1 . ( the Element of D1, the Element of D1)))),(f2 . (a2,(g2 . (a2,b2))))] by Th21 ;

hence f2 . (a2,(g2 . (a2,b2))) = a2 by XTUPLE_0:1; :: thesis: verum

for f2, g2 being BinOp of D2 holds

( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )

let f1, g1 be BinOp of D1; :: thesis: for f2, g2 being BinOp of D2 holds

( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )

let f2, g2 be BinOp of D2; :: thesis: ( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )

defpred S

thus ( f1 absorbs g1 & f2 absorbs g2 implies |:f1,f2:| absorbs |:g1,g2:| ) :: thesis: ( |:f1,f2:| absorbs |:g1,g2:| implies ( f1 absorbs g1 & f2 absorbs g2 ) )

proof

assume A4:
for a, b being Element of [:D1,D2:] holds |:f1,f2:| . (a,(|:g1,g2:| . (a,b))) = a
; :: according to LATTICE2:def 1 :: thesis: ( f1 absorbs g1 & f2 absorbs g2 )
assume A1:
for a1, b1 being Element of D1 holds f1 . (a1,(g1 . (a1,b1))) = a1
; :: according to LATTICE2:def 1 :: thesis: ( not f2 absorbs g2 or |:f1,f2:| absorbs |:g1,g2:| )

assume A2: for a2, b2 being Element of D2 holds f2 . (a2,(g2 . (a2,b2))) = a2 ; :: according to LATTICE2:def 1 :: thesis: |:f1,f2:| absorbs |:g1,g2:|

A3: for d1, d19 being Element of D1

for d2, d29 being Element of D2 holds S_{1}[[d1,d2],[d19,d29]]
_{1}[a,b]
from FILTER_1:sch 5(A3); :: according to LATTICE2:def 1 :: thesis: verum

end;assume A2: for a2, b2 being Element of D2 holds f2 . (a2,(g2 . (a2,b2))) = a2 ; :: according to LATTICE2:def 1 :: thesis: |:f1,f2:| absorbs |:g1,g2:|

A3: for d1, d19 being Element of D1

for d2, d29 being Element of D2 holds S

proof

thus
for a, b being Element of [:D1,D2:] holds S
let a1, b1 be Element of D1; :: thesis: for d2, d29 being Element of D2 holds S_{1}[[a1,d2],[b1,d29]]

let a2, b2 be Element of D2; :: thesis: S_{1}[[a1,a2],[b1,b2]]

thus |:f1,f2:| . ([a1,a2],(|:g1,g2:| . ([a1,a2],[b1,b2]))) = |:f1,f2:| . ([a1,a2],[(g1 . (a1,b1)),(g2 . (a2,b2))]) by Th21

.= [(f1 . (a1,(g1 . (a1,b1)))),(f2 . (a2,(g2 . (a2,b2))))] by Th21

.= [a1,(f2 . (a2,(g2 . (a2,b2))))] by A1

.= [a1,a2] by A2 ; :: thesis: verum

end;let a2, b2 be Element of D2; :: thesis: S

thus |:f1,f2:| . ([a1,a2],(|:g1,g2:| . ([a1,a2],[b1,b2]))) = |:f1,f2:| . ([a1,a2],[(g1 . (a1,b1)),(g2 . (a2,b2))]) by Th21

.= [(f1 . (a1,(g1 . (a1,b1)))),(f2 . (a2,(g2 . (a2,b2))))] by Th21

.= [a1,(f2 . (a2,(g2 . (a2,b2))))] by A1

.= [a1,a2] by A2 ; :: thesis: verum

thus for a1, b1 being Element of D1 holds f1 . (a1,(g1 . (a1,b1))) = a1 :: according to LATTICE2:def 1 :: thesis: f2 absorbs g2

proof

set a1 = the Element of D1;
set a2 = the Element of D2;

let a1, b1 be Element of D1; :: thesis: f1 . (a1,(g1 . (a1,b1))) = a1

[a1, the Element of D2] = |:f1,f2:| . ([a1, the Element of D2],(|:g1,g2:| . ([a1, the Element of D2],[b1, the Element of D2]))) by A4

.= |:f1,f2:| . ([a1, the Element of D2],[(g1 . (a1,b1)),(g2 . ( the Element of D2, the Element of D2))]) by Th21

.= [(f1 . (a1,(g1 . (a1,b1)))),(f2 . ( the Element of D2,(g2 . ( the Element of D2, the Element of D2))))] by Th21 ;

hence f1 . (a1,(g1 . (a1,b1))) = a1 by XTUPLE_0:1; :: thesis: verum

end;let a1, b1 be Element of D1; :: thesis: f1 . (a1,(g1 . (a1,b1))) = a1

[a1, the Element of D2] = |:f1,f2:| . ([a1, the Element of D2],(|:g1,g2:| . ([a1, the Element of D2],[b1, the Element of D2]))) by A4

.= |:f1,f2:| . ([a1, the Element of D2],[(g1 . (a1,b1)),(g2 . ( the Element of D2, the Element of D2))]) by Th21

.= [(f1 . (a1,(g1 . (a1,b1)))),(f2 . ( the Element of D2,(g2 . ( the Element of D2, the Element of D2))))] by Th21 ;

hence f1 . (a1,(g1 . (a1,b1))) = a1 by XTUPLE_0:1; :: thesis: verum

let a2 be Element of D2; :: according to LATTICE2:def 1 :: thesis: for b

let b2 be Element of D2; :: thesis: f2 . (a2,(g2 . (a2,b2))) = a2

[ the Element of D1,a2] = |:f1,f2:| . ([ the Element of D1,a2],(|:g1,g2:| . ([ the Element of D1,a2],[ the Element of D1,b2]))) by A4

.= |:f1,f2:| . ([ the Element of D1,a2],[(g1 . ( the Element of D1, the Element of D1)),(g2 . (a2,b2))]) by Th21

.= [(f1 . ( the Element of D1,(g1 . ( the Element of D1, the Element of D1)))),(f2 . (a2,(g2 . (a2,b2))))] by Th21 ;

hence f2 . (a2,(g2 . (a2,b2))) = a2 by XTUPLE_0:1; :: thesis: verum