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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (AttributeDerivation C) or x in the carrier of (BoolePoset the carrier of C) )
assume x in rng (AttributeDerivation C) ; :: thesis: x in the carrier of (BoolePoset the carrier of C)
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: verum

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 (AttributeDerivation C)

proof

let x be object ; :: thesis: ( x in the carrier of (BoolePoset the carrier' of C) implies x in dom (AttributeDerivation C) )
assume x in the carrier of (BoolePoset the carrier' of C) ; :: thesis: x in dom (AttributeDerivation C)
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 (AttributeDerivation C) by FUNCT_2:def 1; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in dom (AttributeDerivation C) implies x in the carrier of (BoolePoset the carrier' of C) )
assume x in dom (AttributeDerivation C) ; :: thesis: x in the carrier of (BoolePoset the carrier' of C)
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: verum

end;

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