A1: rng (ObjectDerivation C) c= the carrier of (BoolePoset the carrier' of C)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (ObjectDerivation C) ; :: thesis:
then x in bool the carrier' of C ;
then A2: x in the carrier of (BooleLatt the carrier' of C) by LATTICE3:def 1;
LattPOSet (BooleLatt the carrier' of C) = RelStr(# the carrier of (BooleLatt the carrier' of C),(LattRel (BooleLatt the carrier' of C)) #) by LATTICE3:def 2;
hence x in the carrier of (BoolePoset the carrier' of C) by A2, YELLOW_1:def 2; :: thesis:

end;

A3: LattPOSet (BooleLatt the carrier of C) = RelStr(# the carrier of (BooleLatt the carrier of C),(LattRel (BooleLatt the carrier of C)) #) by LATTICE3:def 2;
A4: for x being object st x in the carrier of (BoolePoset the carrier of C) holds
x in dom (ObjectDerivation C)

proof

let x be object ; :: thesis:
assume x in the carrier of (BoolePoset the carrier of C) ; :: thesis:
then x in the carrier of (LattPOSet (BooleLatt the carrier of C)) by YELLOW_1:def 2;
then x in bool the carrier of C by A3, LATTICE3:def 1;
hence x in dom (ObjectDerivation C) by FUNCT_2:def 1; :: thesis:

end;

for x being object st x in dom (ObjectDerivation C) holds
x in the carrier of (BoolePoset the carrier of C)

proof

let x be object ; :: thesis:
assume x in dom (ObjectDerivation C) ; :: thesis:
then x in bool the carrier of C ;
then x in the carrier of (BooleLatt the carrier of C) by LATTICE3:def 1;
hence x in the carrier of (BoolePoset the carrier of C) by A3, YELLOW_1:def 2; :: thesis:

end;

then dom (ObjectDerivation C) = the carrier of (BoolePoset the carrier of C) by A4, TARSKI:2;
then reconsider g = ObjectDerivation C as Function of the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C) by A1, FUNCT_2:def 1, RELSET_1:4;
g is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) ;
hence ObjectDerivation C is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) ; :: thesis: