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

now :: thesis: for t being Element of S holds g1 . t = g2 . t

let t be Element of S; :: thesis: g1 . t = g2 . t
reconsider t9 = t as Element of S ;
A6: g1 . t9 is_maximum_of d " (downarrow t) by A4, WAYBEL_1:11;
A7: g2 . t9 is_maximum_of d " (downarrow t) by A5, WAYBEL_1:11;
g1 . t = "\/" ((d " (downarrow t)),T) by A6;
hence g1 . t = g2 . t by A7; :: thesis: verum

end;

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