let u1, u2 be Element of 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 u1 = 1. L ) & ( c is odd implies u1 = - (1. L) ) ) ) & ( 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 u2 = 1. L ) & ( c is odd implies u2 = - (1. L) ) ) ) implies u1 = u2 )
assume that
A3: 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 u1 = 1. L ) & ( c is odd implies u1 = - (1. L) ) ) and
A4: 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 u2 = 1. L ) & ( c is odd implies u2 = - (1. L) ) ) ; :: thesis: u1 = u2
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 A5: card X is even ; :: thesis: u1 = u2

hence u1 = 1. L by A3
.= u2 by A5, A4 ;
:: thesis: verum

end;

suppose A6: card X is odd ; :: thesis: u1 = u2

hence u1 = - (1. L) by A3
.= u2 by A6, A4 ;
:: thesis: verum

end;

end;