let o1, o2 be BinOp of Subgroups G; :: thesis: ( ( for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
o1 . S1,S2 = H1 /\ H2 ) & ( for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
o2 . S1,S2 = H1 /\ H2 ) implies o1 = o2 )
assume A2: for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
o1 . S1,S2 = H1 /\ H2 ; :: thesis: ( ex S1, S2 being Element of Subgroups G ex H1, H2 being Subgroup of G st
( S1 = H1 & S2 = H2 & not o2 . S1,S2 = H1 /\ H2 ) or o1 = o2 )
assume A3: for S1, S2 being Element of Subgroups G
for H1, H2 being Subgroup of G st S1 = H1 & S2 = H2 holds
o2 . S1,S2 = H1 /\ H2 ; :: thesis: o1 = o2

now

let x, y be set ; :: thesis: ( x in Subgroups G & y in Subgroups G implies o1 . x,y = o2 . x,y )
assume A4: ( 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 Subgroup of G by A4, GROUP_3:def 1;
( o1 . A,B = H1 /\ H2 & o2 . A,B = H1 /\ H2 ) by A2, A3;
hence o1 . x,y = o2 . x,y ; :: thesis: verum

end;

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