let o1, o2 be BinOp of (OSSub U0); :: thesis: ( ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 /\ U2 ) implies o1 = o2 )
assume that
A3: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 /\ U2 and
A4: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 /\ U2 ; :: thesis: o1 = o2
for x, y being Element of OSSub U0 holds o1 . (x,y) = o2 . (x,y)

proof

let x, y be Element of OSSub U0; :: thesis: o1 . (x,y) = o2 . (x,y)
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
o1 . (x,y) = U1 /\ U2 by A3;
hence o1 . (x,y) = o2 . (x,y) by A4; :: thesis: verum

end;

hence o1 = o2 by BINOP_1:2; :: thesis: verum