let o1, o2 be BinOp of (MSSub U0); :: thesis: ( ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . x,y = U1 "\/" U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra 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 MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . x,y = U1 "\/" U2 and
A4: for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . x,y = U1 "\/" U2 ; :: thesis: o1 = o2
for x, y being Element of MSSub U0 holds o1 . x,y = o2 . x,y

proof

let x, y be Element of MSSub U0; :: thesis: o1 . x,y = o2 . x,y
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def20;
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