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 "\/"_os 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 "\/"_os U2 ) implies o1 = o2 )
assume 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 "\/"_os 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 "\/"_os 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 Def15;
( o1 . x,y = U1 "\/"_os U2 & o2 . x,y = U1 "\/"_os U2 ) by A3;
hence o1 . x,y = o2 . x,y ; :: thesis: verum

end;

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