let F1, F2 be Function of (Subgroups G),(bool the carrier of G); :: thesis: ( ( for H being strict Subgroup of G holds F1 . H = the carrier of H ) & ( for H being strict Subgroup of G holds F2 . H = the carrier of H ) implies F1 = F2 )
assume that
A3: for H1 being strict Subgroup of G holds F1 . H1 = the carrier of H1 and
A4: for H2 being strict Subgroup of G holds F2 . H2 = the carrier of H2 ; :: thesis: F1 = F2
for h being object st h in Subgroups G holds
F1 . h = F2 . h

proof

let h be object ; :: thesis: ( h in Subgroups G implies F1 . h = F2 . h )
assume h in Subgroups G ; :: thesis: F1 . h = F2 . h
then reconsider H = h as strict Subgroup of G by GROUP_3:def 1;
thus F1 . h = the carrier of H by A3
.= F2 . h by A4 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:12; :: thesis: verum