let S be non empty finite set ; :: thesis: for s being Element of S *
for f being Function of S,BOOLEAN holds Coim ((('not' f) * s),TRUE) = (dom s) \ (Coim ((f * s),TRUE))
let s be Element of S * ; :: thesis: for f being Function of S,BOOLEAN holds Coim ((('not' f) * s),TRUE) = (dom s) \ (Coim ((f * s),TRUE))
let f be Function of S,BOOLEAN; :: thesis: Coim ((('not' f) * s),TRUE) = (dom s) \ (Coim ((f * s),TRUE))

A1: now :: thesis: for x being object holds
( x in ('not' f) " {TRUE} iff x in (dom f) \ (f " {TRUE}) )

let x be object ; :: thesis: ( x in ('not' f) " {TRUE} iff x in (dom f) \ (f " {TRUE}) )
A2: ( f . x = FALSE iff not f . x = TRUE ) by XBOOLEAN:def 3;
A3: ( x in dom ('not' f) iff x in dom f ) by MARGREL1:def 17;
A4: ( x in ('not' f) " {TRUE} iff ( x in dom ('not' f) & ('not' f) . x in {TRUE} ) ) by FUNCT_1:def 7;
( x in dom ('not' f) & ('not' f) . x = TRUE iff ( x in dom f & not f . x = TRUE ) ) by Lm4, A3, A2;
then ( x in ('not' f) " {TRUE} iff ( x in dom f & ( not x in dom f or not f . x in {TRUE} ) ) ) by A4, TARSKI:def 1;
then ( x in ('not' f) " {TRUE} iff ( x in dom f & not x in f " {TRUE} ) ) by FUNCT_1:def 7;
hence ( x in ('not' f) " {TRUE} iff x in (dom f) \ (f " {TRUE}) ) by XBOOLE_0:def 5; :: thesis: verum

end;

dom f = S by FUNCT_2:def 1;
then A5: (rng s) /\ (dom f) = rng s by XBOOLE_1:28;
s " (dom f) = s " ((rng s) /\ (dom f)) by RELAT_1:133;
then A6: s " (dom f) = dom s by A5, RELAT_1:134;
thus Coim ((('not' f) * s),TRUE) = s " (('not' f) " {TRUE}) by RELAT_1:146
.= s " ((dom f) \ (f " {TRUE})) by A1, TARSKI:2
.= (s " (dom f)) \ (s " (f " {TRUE})) by FUNCT_1:69
.= (dom s) \ (Coim ((f * s),TRUE)) by A6, RELAT_1:146 ; :: thesis: verum