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)

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

hence
o1 = o2
by BINOP_1:2; :: thesis: verum
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 Def19;

o1 . (x,y) = U1 "\/" U2 by A3;

hence o1 . (x,y) = o2 . (x,y) by A4; :: thesis: verum

end;reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;

o1 . (x,y) = U1 "\/" U2 by A3;

hence o1 . (x,y) = o2 . (x,y) by A4; :: thesis: verum