let C be FormalContext; :: thesis: for o being Object of C holds (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a }
let o be Object of C; :: thesis: (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a }
{o} c= the carrier of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {o} or x in the carrier of C )
assume x in {o} ; :: thesis: x in the carrier of C
then x = o by TARSKI:def 1;
hence x in the carrier of C ; :: thesis: verum

end;

then reconsider t = {o} as Subset of the carrier of C ;
A1: for x being object st x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } holds
x in { a where a is Attribute of C : o is-connected-with a }

proof

set o9 = the Element of t;
let x be object ; :: thesis: ( x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } implies x in { a where a is Attribute of C : o is-connected-with a } )
reconsider o9 = the Element of t as Object of C by TARSKI:def 1;
A2: o9 = o by TARSKI:def 1;
assume x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } ; :: thesis: x in { a where a is Attribute of C : o is-connected-with a }
then A3: ex x9 being Attribute of C st
( x9 = x & ( for o9 being Object of C st o9 in t holds
o9 is-connected-with x9 ) ) ;
then reconsider x = x as Attribute of C ;
o9 is-connected-with x by A3;
hence x in { a where a is Attribute of C : o is-connected-with a } by A2; :: thesis: verum

end;

A4: for x being object st x in { a where a is Attribute of C : o is-connected-with a } holds
x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a }

proof

let x be object ; :: thesis: ( x in { a where a is Attribute of C : o is-connected-with a } implies x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } )
assume x in { a where a is Attribute of C : o is-connected-with a } ; :: thesis: x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a }
then A5: ex x9 being Attribute of C st
( x9 = x & o is-connected-with x9 ) ;
then reconsider x = x as Attribute of C ;
for o9 being Object of C st o9 in t holds
o9 is-connected-with x by A5, TARSKI:def 1;
hence x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } ; :: thesis: verum

end;

(ObjectDerivation C) . t = { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } by Def2;
hence (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a } by A1, A4, TARSKI:2; :: thesis: verum