let C be FormalContext; :: thesis: for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O
let O be Subset of the carrier of C; :: thesis: (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O
reconsider O9 = O as Subset of the carrier' of (C .:) ;
set A1 = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
set A2 = { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } ;
A1: { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } c= { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o }

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } or u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } )
assume u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; :: thesis: u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o }
then consider a being Attribute of C such that
A2: a = u and
A3: for o being Object of C st o in O holds
o is-connected-with a ;
reconsider u9 = u as Object of (C .:) by A2;
for o9 being Attribute of (C .:) st o9 in O9 holds
u9 is-connected-with o9

proof

let o9 be Attribute of (C .:); :: thesis: ( o9 in O9 implies u9 is-connected-with o9 )
reconsider o = o9 as Object of C ;
assume o9 in O9 ; :: thesis: u9 is-connected-with o9
then o is-connected-with a by A3;
then [o,a] in the Information of C by CONLAT_1:def 2;
then [a,o] in the Information of (C .:) by RELAT_1:def 7;
hence u9 is-connected-with o9 by A2, CONLAT_1:def 2; :: thesis: verum

end;

hence u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } ; :: thesis: verum

end;

A4: { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } c= { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } or u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } )
assume u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } ; :: thesis: u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
then consider a being Object of (C .:) such that
A5: a = u and
A6: for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o ;
reconsider u9 = u as Attribute of C by A5;
for o being Object of C st o in O holds
o is-connected-with u9

proof

let o9 be Object of C; :: thesis: ( o9 in O implies o9 is-connected-with u9 )
reconsider o = o9 as Attribute of (C .:) ;
assume o9 in O ; :: thesis: o9 is-connected-with u9
then a is-connected-with o by A6;
then [a,o] in the Information of (C .:) by CONLAT_1:def 2;
then [o9,u9] in the Information of C by A5, RELAT_1:def 7;
hence o9 is-connected-with u9 by CONLAT_1:def 2; :: thesis: verum

end;

hence u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; :: thesis: verum

end;

( (ObjectDerivation C) . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } & (AttributeDerivation (C .:)) . O9 = { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } ) by CONLAT_1:def 3, CONLAT_1:def 4;
hence (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O by A1, A4; :: thesis: verum