let C be FormalContext; :: thesis: for A1, A2 being Subset of the carrier' of C holds (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
let A1, A2 be Subset of the carrier' of C; :: thesis: (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
reconsider A9 = A1 \/ A2 as Subset of the carrier' of C ;
A1: for x being object st x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) holds
x in (AttributeDerivation C) . A9

proof

let x be object ; :: thesis: ( x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) implies x in (AttributeDerivation C) . A9 )
assume A2: x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) ; :: thesis: x in (AttributeDerivation C) . A9
then x in (AttributeDerivation C) . A1 by XBOOLE_0:def 4;
then x in { o where o is Object of C : for a being Attribute of C st a in A1 holds
o is-connected-with a } by Def3;
then A3: ex x1 being Object of C st
( x1 = x & ( for a being Attribute of C st a in A1 holds
x1 is-connected-with a ) ) ;
x in (AttributeDerivation C) . A2 by A2, XBOOLE_0:def 4;
then x in { o where o is Object of C : for a being Attribute of C st a in A2 holds
o is-connected-with a } by Def3;
then A4: ex x2 being Object of C st
( x2 = x & ( for a being Attribute of C st a in A2 holds
x2 is-connected-with a ) ) ;
then reconsider x = x as Object of C ;
for a being Attribute of C st a in A1 \/ A2 holds
x is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a in A1 \/ A2 implies x is-connected-with a )
assume A5: a in A1 \/ A2 ; :: thesis: x is-connected-with a

now :: thesis: ( ( a in A1 & x is-connected-with a ) or ( a in A2 & x is-connected-with a ) )

per cases ( a in A1 or a in A2 ) by A5, XBOOLE_0:def 3;

case a in A1 ; :: thesis: x is-connected-with a

hence x is-connected-with a by A3; :: thesis: verum

end;

case a in A2 ; :: thesis: x is-connected-with a

hence x is-connected-with a by A4; :: thesis: verum

end;

end;

end;

hence x is-connected-with a ; :: thesis: verum

end;

then x in { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ;
hence x in (AttributeDerivation C) . A9 by Def3; :: thesis: verum

end;

for x being object st x in (AttributeDerivation C) . (A1 \/ A2) holds
x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)

proof

let x be object ; :: thesis: ( x in (AttributeDerivation C) . (A1 \/ A2) implies x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) )
assume x in (AttributeDerivation C) . (A1 \/ A2) ; :: thesis: x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
then x in { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } by Def3;
then A6: ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in A9 holds
x9 is-connected-with a ) ) ;
then reconsider x = x as Object of C ;
for a being Attribute of C st a in A2 holds
x is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a in A2 implies x is-connected-with a )
assume a in A2 ; :: thesis: x is-connected-with a
then a in A9 by XBOOLE_0:def 3;
hence x is-connected-with a by A6; :: thesis: verum

end;

then x in { o where o is Object of C : for a being Attribute of C st a in A2 holds
o is-connected-with a } ;
then A7: x in (AttributeDerivation C) . A2 by Def3;
for a being Attribute of C st a in A1 holds
x is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a in A1 implies x is-connected-with a )
assume a in A1 ; :: thesis: x is-connected-with a
then a in A9 by XBOOLE_0:def 3;
hence x is-connected-with a by A6; :: thesis: verum

end;

then x in { o where o is Object of C : for a being Attribute of C st a in A1 holds
o is-connected-with a } ;
then x in (AttributeDerivation C) . A1 by Def3;
hence x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) by A7, XBOOLE_0:def 4; :: thesis: verum

end;

hence (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) by A1, TARSKI:2; :: thesis: verum