let L be doubleLoopStr ; :: thesis: for f being finite Function
for E being Function holds
( SgnMembershipNumber (f,L,E) = 1. L or SgnMembershipNumber (f,L,E) = - (1. L) )
let f be finite Function; :: thesis: for E being Function holds
( SgnMembershipNumber (f,L,E) = 1. L or SgnMembershipNumber (f,L,E) = - (1. L) )
let E be Function; :: thesis: ( SgnMembershipNumber (f,L,E) = 1. L or SgnMembershipNumber (f,L,E) = - (1. L) )
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 y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } or y in dom f )
assume y in { x where x is Element of dom f : ( x in dom f & f . x in E . x ) } ; :: thesis: y in dom f
then ex x being Element of dom f st
( x = y & x in dom f & f . x in E . x ) ;
hence y 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 ;
( card X is even or card X is odd ) ;
hence ( SgnMembershipNumber (f,L,E) = 1. L or SgnMembershipNumber (f,L,E) = - (1. L) ) by Def9; :: thesis: verum