let F1, F2 be BinOp of (B-carrier C); :: thesis: ( ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . (CP1,CP2) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . (CP1,CP2) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 ) ) implies F1 = F2 )
assume A4: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . (CP1,CP2) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 ) ; :: thesis: ( ex CP1, CP2 being strict FormalConcept of C st
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( not F2 . (CP1,CP2) = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) or not A = the Intent of CP1 /\ the Intent of CP2 ) or F1 = F2 )
assume A5: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . (CP1,CP2) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 ) ; :: thesis: F1 = F2
A6: for X being object st X in [:(B-carrier C),(B-carrier C):] holds
F1 . X = F2 . X

proof

let X be object ; :: thesis: ( X in [:(B-carrier C),(B-carrier C):] implies F1 . X = F2 . X )
assume X in [:(B-carrier C),(B-carrier C):] ; :: thesis: F1 . X = F2 . X
then consider A, B being object such that
A7: A in B-carrier C and
A8: B in B-carrier C and
A9: X = [A,B] by ZFMISC_1:def 2;
reconsider B = B as strict FormalConcept of C by A8, Th31;
reconsider A = A as strict FormalConcept of C by A7, Th31;
( ex O being Subset of the carrier of C ex At being Subset of the carrier' of C st
( F1 . (A,B) = ConceptStr(# O,At #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of A \/ the Extent of B)) & At = the Intent of A /\ the Intent of B ) & ex O9 being Subset of the carrier of C ex At9 being Subset of the carrier' of C st
( F2 . (A,B) = ConceptStr(# O9,At9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of A \/ the Extent of B)) & At9 = the Intent of A /\ the Intent of B ) ) by A4, A5;
hence F1 . X = F2 . X by A9; :: thesis: verum

end;

( dom F1 = [:(B-carrier C),(B-carrier C):] & dom F2 = [:(B-carrier C),(B-carrier C):] ) by FUNCT_2:def 1;
hence F1 = F2 by A6, FUNCT_1:2; :: thesis: verum