let C be FormalContext; :: thesis: for CP1, CP2, CP3 being strict FormalConcept of C holds (B-join C) . CP1,((B-join C) . CP2,CP3) = (B-join C) . ((B-join C) . CP1,CP2),CP3
let CP1, CP2, CP3 be strict FormalConcept of C; :: thesis: (B-join C) . CP1,((B-join C) . CP2,CP3) = (B-join C) . ((B-join C) . CP1,CP2),CP3
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A1: ( (B-join C) . 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 ) by Def22;
(B-join C) . CP1,CP2 in rng (B-join C) by Lm3;
then reconsider CP = (B-join C) . CP1,CP2 as strict FormalConcept of C by Th35;
consider O' being Subset of the carrier of C, A' being Subset of the carrier' of C such that
A2: ( (B-join C) . CP,CP3 = ConceptStr(# O',A' #) & O' = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP \/ the Extent of CP3)) & A' = the Intent of CP /\ the Intent of CP3 ) by Def22;
(B-join C) . CP,CP3 in rng (B-join C) by Lm3;
then reconsider CPa = (B-join C) . CP,CP3 as strict FormalConcept of C by Th35;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A3: ( (B-join C) . CP2,CP3 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP2 \/ the Extent of CP3)) & A = the Intent of CP2 /\ the Intent of CP3 ) by Def22;
(B-join C) . CP2,CP3 in rng (B-join C) by Lm3;
then reconsider CP' = (B-join C) . CP2,CP3 as strict FormalConcept of C by Th35;
consider O' being Subset of the carrier of C, A' being Subset of the carrier' of C such that
A4: ( (B-join C) . CP1,CP' = ConceptStr(# O',A' #) & O' = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP')) & A' = the Intent of CP1 /\ the Intent of CP' ) by Def22;
(B-join C) . CP1,CP' in rng (B-join C) by Lm3;
then reconsider CPb = (B-join C) . CP1,CP' as strict FormalConcept of C by Th35;
the Extent of CPa = the Extent of CPb

proof

(AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP2 \/ the Extent of CP3))))) = (AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP2 \/ the Extent of CP3))))) by Th16
.= (AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . (the Extent of CP2 \/ the Extent of CP3))) by Th7
.= (AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ (((ObjectDerivation C) . the Extent of CP2) /\ ((ObjectDerivation C) . the Extent of CP3))) by Th16
.= (AttributeDerivation C) . ((((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP3)) by XBOOLE_1:16
.= (AttributeDerivation C) . (((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP3)) by Th16
.= (AttributeDerivation C) . (((ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)))) /\ ((ObjectDerivation C) . the Extent of CP3)) by Th7
.= (AttributeDerivation C) . ((ObjectDerivation C) . (((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) \/ the Extent of CP3)) by Th16 ;
hence the Extent of CPa = the Extent of CPb by A1, A2, A3, A4; :: thesis: verum

end;

hence (B-join C) . CP1,((B-join C) . CP2,CP3) = (B-join C) . ((B-join C) . CP1,CP2),CP3 by A1, A2, A3, A4, XBOOLE_1:16; :: thesis: verum