let C be FormalContext; :: thesis: for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (ObjectDerivation (C .: )) . A
let O be Subset of the carrier' of C; :: thesis: (AttributeDerivation C) . O = (ObjectDerivation (C .: )) . O
A1: (AttributeDerivation C) . O = { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } by CONLAT_1:def 7;
reconsider O' = O as Subset of the carrier of (C .: ) ;
A2: (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 } by CONLAT_1:def 6;
set A1 = { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } ;
set A2 = { a where a is Attribute of (C .: ) : for o being Object of (C .: ) st o in O' holds
o is-connected-with a } ;
A3: { a where a is Object of C : for o being Attribute of C st o in O 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 set ; :: 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 O 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 O 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
A4: ( a = u & ( for o being Attribute of C st o in O holds
a is-connected-with o ) ) ;
reconsider u' = u as Attribute of (C .: ) by A4;
for o being Object of (C .: ) st o in O' holds
o is-connected-with u'

proof

let o' be Object of (C .: ); :: thesis: ( o' in O' implies o' is-connected-with u' )
assume A5: o' in O' ; :: thesis: o' is-connected-with u'
reconsider o = o' as Attribute of C ;
a is-connected-with o by A4, A5;
then [a,o] in the Information of C by CONLAT_1:def 5;
then [o',u'] in the Information of (C .: ) by A4, RELAT_1:def 7;
hence o' is-connected-with u' by CONLAT_1:def 5; :: 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;

{ 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 O holds
a is-connected-with o }

proof

let u be set ; :: 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 O 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 O holds
a is-connected-with o }
then consider a being Attribute of (C .: ) such that
A6: ( a = u & ( for o being Object of (C .: ) st o in O' holds
o is-connected-with a ) ) ;
reconsider u' = u as Object of C by A6;
for o being Attribute of C st o in O holds
u' is-connected-with o

proof

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

end;

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

end;

hence (AttributeDerivation C) . O = (ObjectDerivation (C .: )) . O by A1, A2, A3, XBOOLE_0:def 10; :: thesis: verum