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 A69: 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 A70: for CP being strict FormalConcept of C holds F2 . CP = CP .: ; :: thesis: F1 = F2
A71: for u being object st u in the carrier of ((ConceptLattice C) .:) holds
F1 . u = F2 . u
proof
let u be object ; :: thesis: ( u in the carrier of ((ConceptLattice C) .:) implies F1 . u = F2 . u )
ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 20;
then A72: (ConceptLattice C) .: = LattStr(# (B-carrier C),(B-meet C),(B-join C) #) by LATTICE2:def 2;
assume u in the carrier of ((ConceptLattice C) .:) ; :: thesis: F1 . u = F2 . u
then reconsider u = u as strict FormalConcept of C by A72, CONLAT_1:31;
F1 . u = u .: by A69
.= F2 . u by A70 ;
hence F1 . u = F2 . u ; :: thesis: verum
end;
( dom F1 = the carrier of ((ConceptLattice C) .:) & dom F2 = the carrier of ((ConceptLattice C) .:) ) by FUNCT_2:def 1;
hence F1 = F2 by A71; :: thesis: verum