let F1, F2 be Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .: ); :: thesis: ( ( for CP being strict FormalConcept of C holds F1 . CP = CP .: ) & ( for CP being strict FormalConcept of C holds F2 . CP = CP .: ) implies F1 = F2 )
assume A65: for CP being strict FormalConcept of C holds F1 . CP = CP .: ; :: thesis: ( ex CP being strict FormalConcept of C st not F2 . CP = CP .: or F1 = F2 )
assume A66: for CP being strict FormalConcept of C holds F2 . CP = CP .: ; :: thesis: F1 = F2
A67: for u being set st u in the carrier of ((ConceptLattice C) .: ) holds
F1 . u = F2 . u

proof

let u be set ; :: thesis: ( u in the carrier of ((ConceptLattice C) .: ) implies F1 . u = F2 . u )
assume A68: u in the carrier of ((ConceptLattice C) .: ) ; :: thesis: F1 . u = F2 . u
ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 23;
then (ConceptLattice C) .: = LattStr(# (B-carrier C),(B-meet C),(B-join C) #) by LATTICE2:def 2;
then reconsider u = u as strict FormalConcept of C by A68, CONLAT_1:35;
F1 . u = u .: by A65
.= F2 . u by A66 ;
hence F1 . u = F2 . u ; :: thesis: verum

end;

A69: dom F1 = the carrier of ((ConceptLattice C) .: ) by FUNCT_2:def 1;
dom F2 = the carrier of ((ConceptLattice C) .: ) by FUNCT_2:def 1;
hence F1 = F2 by A67, A69, FUNCT_1:9; :: thesis: verum