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

now

let t be Element of T; :: thesis: d1 . t = d2 . t
reconsider t' = t as Element of T ;
( d1 . t' is_minimum_of g " (uparrow t) & d2 . t' is_minimum_of g " (uparrow t) ) by A2, A3, WAYBEL_1:11;
then ( d1 . t = "/\" (g " (uparrow t)),S & d2 . t = "/\" (g " (uparrow t)),S ) by WAYBEL_1:def 6;
hence d1 . t = d2 . t ; :: thesis: verum

end;

hence d1 = d2 by FUNCT_2:113; :: thesis: verum