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 :: thesis: for x being Element of H holds g1 . x = g2 . x

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

end;

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