let o1, o2 be BinOp of (Subgroups G); :: thesis: ( ( for H1, H2 being strict Subgroup of G holds o1 . (H1,H2) = H1 "\/" H2 ) & ( for H1, H2 being strict Subgroup of G holds o2 . (H1,H2) = H1 "\/" H2 ) implies o1 = o2 )
assume that
A3: for H1, H2 being strict Subgroup of G holds o1 . (H1,H2) = H1 "\/" H2 and
A4: for H1, H2 being strict Subgroup of G holds o2 . (H1,H2) = H1 "\/" H2 ; :: thesis: o1 = o2

now :: thesis: for x, y being set st x in Subgroups G & y in Subgroups G holds
o1 . (x,y) = o2 . (x,y)

let x, y be set ; :: thesis: ( x in Subgroups G & y in Subgroups G implies o1 . (x,y) = o2 . (x,y) )
assume A5: ( x in Subgroups G & y in Subgroups G ) ; :: thesis: o1 . (x,y) = o2 . (x,y)
then reconsider A = x, B = y as Element of Subgroups G ;
reconsider H1 = x, H2 = y as strict Subgroup of G by A5, GROUP_3:def 1;
o1 . (A,B) = H1 "\/" H2 by A3;
hence o1 . (x,y) = o2 . (x,y) by A4; :: thesis: verum

end;

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