set X = { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } ;
{ x where x is Element of dom f : ( x in dom f & f . x in E . x ) } c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } or x in dom f )
assume x in { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } ; :: thesis: x in dom f
then ex y being Element of dom f st
( x = y & y in dom f & f . y in E . y ) ;
hence x in dom f ; :: thesis: verum

end;

then reconsider X = { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } as finite set ;

per cases ( card X is even or card X is odd ) ;

suppose A1: card X is even ; :: thesis: ex b₁ being Element of L st
for c being Nat st c = card { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } holds
( ( c is even implies b₁ = 1. L ) & ( c is odd implies b₁ = - (1. L) ) )

take 1. L ; :: thesis: for c being Nat st c = card { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } holds
( ( c is even implies 1. L = 1. L ) & ( c is odd implies 1. L = - (1. L) ) )
thus for c being Nat st c = card { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } holds
( ( c is even implies 1. L = 1. L ) & ( c is odd implies 1. L = - (1. L) ) ) by A1; :: thesis: verum

end;

suppose A2: card X is odd ; :: thesis: ex b₁ being Element of L st
for c being Nat st c = card { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } holds
( ( c is even implies b₁ = 1. L ) & ( c is odd implies b₁ = - (1. L) ) )

take - (1. L) ; :: thesis: for c being Nat st c = card { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } holds
( ( c is even implies - (1. L) = 1. L ) & ( c is odd implies - (1. L) = - (1. L) ) )
thus for c being Nat st c = card { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } holds
( ( c is even implies - (1. L) = 1. L ) & ( c is odd implies - (1. L) = - (1. L) ) ) by A2; :: thesis: verum

end;

end;