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 :: thesis: for t being Element of T holds d1 . t = d2 . t
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:10;
A7: d2 . t9 is_minimum_of g " (uparrow t) by A5, WAYBEL_1:10;
d1 . t = "/\" ((g " (uparrow t)),S) by A6;
hence d1 . t = d2 . t by A7; :: thesis: verum
end;
hence d1 = d2 by FUNCT_2:63; :: thesis: verum