let g1, g2 be Function of H,H; :: thesis: ( [g1,(a "/\" )] is Galois & [g2,(a "/\" )] is Galois implies g1 = g2 )
assume that
A2: [g1,(a "/\" )] is Galois and
A3: [g2,(a "/\" )] is Galois ; :: thesis: g1 = g2

now

let x be Element of H; :: thesis: g1 . x = g2 . x
H is LATTICE by A1;
then ( g1 . x is_maximum_of (a "/\" ) " (downarrow x) & g2 . x is_maximum_of (a "/\" ) " (downarrow x) ) by A2, A3, Th12;
then ( g1 . x = "\/" ((a "/\" ) " (downarrow x)),H & g2 . x = "\/" ((a "/\" ) " (downarrow x)),H ) by Def7;
hence g1 . x = g2 . x ; :: thesis: verum

end;

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