let f1, f2 be Function of the carrier of (lattice G1), the carrier of (lattice G2); :: thesis: ( ( for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
f1 . H = gr A ) & ( for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
f2 . H = gr A ) implies f1 = f2 )
assume that
A4: for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
f1 . H = gr A and
A5: for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
f2 . H = gr A ; :: thesis: f1 = f2
for h being object st h in the carrier of (lattice G1) holds
f1 . h = f2 . h

proof

let h be object ; :: thesis: ( h in the carrier of (lattice G1) implies f1 . h = f2 . h )
assume h in the carrier of (lattice G1) ; :: thesis: f1 . h = f2 . h
then reconsider H = h as strict Subgroup of G1 by GROUP_3:def 1;
thus f1 . h = gr (f .: the carrier of H) by A4
.= f2 . h by A5 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum