let L be doubleLoopStr ; :: thesis: for E being Function holds SgnMembershipNumber ({},L,E) = 1. L
let E be Function; :: thesis: SgnMembershipNumber ({},L,E) = 1. L
reconsider f = {} as finite Function ;
set X = { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } ;
A1: { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } = {}

proof

assume { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } <> {} ; :: thesis: contradiction
then consider y being object such that
A2: y in { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } by XBOOLE_0:def 1;
ex x being Element of dom f st
( y = x & x in dom f & f . x in E . x ) by A2;
hence contradiction ; :: 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 ;
card X is even by A1;
hence SgnMembershipNumber ({},L,E) = 1. L by Def9; :: thesis: verum