let L be doubleLoopStr ; :: thesis: for f, e being FinSequence
for x being object
for E being set st len f = len e & not x in E holds
SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e)
let f, e be FinSequence; :: thesis: for x being object
for E being set st len f = len e & not x in E holds
SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e)
let x be object ; :: thesis: for E being set st len f = len e & not x in E holds
SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e)
let E be set ; :: thesis: ( len f = len e & not x in E implies SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e) )
assume that
A1: len e = len f and
A2: not x in E ; :: thesis: SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e)
set fx = f ^ <*x*>;
set eX = e ^ <*E*>;
set X1 = { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) } ;
set X = { x where x is Element of dom f : ( x in dom f & f . x in e . x ) } ;
A3: dom f = dom e by A1, FINSEQ_3:29;
{ x where x is Element of dom f : ( x in dom f & f . x in e . x ) } c= dom f

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of dom f : ( x in dom f & f . x in e . x ) } or a in dom f )
assume a in { x where x is Element of dom f : ( x in dom f & f . x in e . x ) } ; :: thesis: a in dom f
then ex x being Element of dom f st
( x = a & x in dom f & f . x in e . x ) ;
hence a 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 ;
A4: X = { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) }

proof

thus X c= { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) } c= X

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) } )
assume a in X ; :: thesis: a in { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) }
then consider x being Element of dom f such that
A5: ( x = a & x in dom f & f . x in e . x ) ;
reconsider x = x as Nat ;
A6: dom f c= dom (f ^ <*x*>) by FINSEQ_1:26;
( (e ^ <*E*>) . x = e . x & (f ^ <*x*>) . x = f . x ) by A5, A3, FINSEQ_1:def 7;
hence a in { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) } by A6, A5; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) } or a in X )
assume a in { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) } ; :: thesis: a in X
then consider y being Element of dom (f ^ <*x*>) such that
A7: ( y = a & y in dom (f ^ <*x*>) & (f ^ <*x*>) . y in (e ^ <*E*>) . y ) ;
reconsider y = y as Nat ;
len <*x*> = 1 by FINSEQ_1:39;
then A8: len (f ^ <*x*>) = (len f) + 1 by FINSEQ_1:22;

per cases ( y = (len f) + 1 or y <> (len f) + 1 ) ;

suppose y = (len f) + 1 ; :: thesis: a in X

hence a in X by A7, A2, A1; :: thesis: verum

end;

suppose A9: y <> (len f) + 1 ; :: thesis: a in X

y <= (len f) + 1 by A8, FINSEQ_3:25;
then y < (len f) + 1 by A9, XXREAL_0:1;
then ( 1 <= y & y <= len f ) by NAT_1:13, FINSEQ_3:25;
then A10: y in dom f by FINSEQ_3:25;
then ( (f ^ <*x*>) . y = f . y & (e ^ <*E*>) . y = e . y ) by A3, FINSEQ_1:def 7;
hence a in X by A7, A10; :: thesis: verum

end;

end;

end;

then reconsider X1 = { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) } as finite set ;

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

suppose card X is even ; :: thesis: SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e)

then ( SgnMembershipNumber (f,L,e) = 1. L & 1. L = SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) ) by Def9, A4;
hence SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e) ; :: thesis: verum

end;

suppose card X is odd ; :: thesis: SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e)

then ( SgnMembershipNumber (f,L,e) = - (1. L) & - (1. L) = SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) ) by Def9, A4;
hence SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e) ; :: thesis: verum

end;

end;