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

now

let t be Element of T; :: thesis: d1 . t = d2 . t
reconsider t9 = t as Element of T ;
A6: d1 . t9 is_minimum_of g " (uparrow t) by A4, WAYBEL_1:11;
A7: d2 . t9 is_minimum_of g " (uparrow t) by A5, WAYBEL_1:11;
d1 . t = "/\" ((g " (uparrow t)),S) by A6, WAYBEL_1:def 6;
hence d1 . t = d2 . t by A7, WAYBEL_1:def 6; :: thesis: verum

end;

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