let g1, g2 be Function of S,T; :: thesis: ( [g1,d] is Galois & [g2,d] is Galois implies g1 = g2 )
assume that
A2: [g1,d] is Galois and
A3: [g2,d] is Galois ; :: thesis: g1 = g2

now

let t be Element of S; :: thesis: g1 . t = g2 . t
reconsider t' = t as Element of S ;
( g1 . t' is_maximum_of d " (downarrow t) & g2 . t' is_maximum_of d " (downarrow t) ) by A2, A3, WAYBEL_1:12;
then ( g1 . t = "\/" (d " (downarrow t)),T & g2 . t = "\/" (d " (downarrow t)),T ) by WAYBEL_1:def 7;
hence g1 . t = g2 . t ; :: thesis: verum

end;

hence g1 = g2 by FUNCT_2:113; :: thesis: verum