let S, T be non empty Poset; :: thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is one-to-one iff d is onto )
let g be Function of S,T; :: thesis: for d being Function of T,S st [g,d] is Galois holds
( g is one-to-one iff d is onto )
let d be Function of T,S; :: thesis: ( [g,d] is Galois implies ( g is one-to-one iff d is onto ) )
assume A1: [g,d] is Galois ; :: thesis: ( g is one-to-one iff d is onto )

hereby :: thesis: ( d is onto implies g is one-to-one )

A2: ( d * g <= id S & id T <= g * d ) by A1, Th18;
( g is monotone & d is monotone ) by A1, Th8;
then A3: g = (g * d) * g by A2, Th20
.= g * (d * g) by RELAT_1:36 ;
A4: ( the carrier of S = dom g & the carrier of S = dom (d * g) ) by FUNCT_2:def 1;
A5: rng (d * g) c= the carrier of S ;
assume g is one-to-one ; :: thesis: d is onto
then d * g = id S by A4, A5, A3, FUNCT_1:28;
hence d is onto by FUNCT_2:23; :: thesis: verum

end;

assume d is onto ; :: thesis: g is one-to-one
then for s being Element of S holds g . s is_maximum_of d " {s} by A1, Th25;
then d * g = id S by Th26;
hence g is one-to-one by FUNCT_2:23; :: thesis: verum