let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for f, e being FinSequence
for x being object
for E being set st len f = len e & 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 & 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 & x in E holds
SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = - (SgnMembershipNumber (f,L,e))
let E be set ; :: thesis: ( len f = len e & x in E implies SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = - (SgnMembershipNumber (f,L,e)) )
assume that
A1: len e = len f and
A2: 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;
A4: { x where x is Element of dom f : ( x in dom f & f . x in e . x ) } c= { x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) }

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 { 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 where x is Element of dom f : ( x in dom f & f . x in e . 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;

{ x where x is Element of dom (f ^ <*x*>) : ( x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) } c= dom (f ^ <*x*>)

proof

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 dom (f ^ <*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 dom (f ^ <*x*>)
then ex x being Element of dom (f ^ <*x*>) st
( x = a & x in dom (f ^ <*x*>) & (f ^ <*x*>) . x in (e ^ <*E*>) . x ) ;
hence a in dom (f ^ <*x*>) ; :: thesis: verum

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 ) } , X = { x where x is Element of dom f : ( x in dom f & f . x in e . x ) } as finite set by A4;
len <*x*> = 1 by FINSEQ_1:39;
then A7: len (f ^ <*x*>) = (len f) + 1 by FINSEQ_1:22;
A8: not (len f) + 1 in X

proof

assume (len f) + 1 in X ; :: thesis: contradiction
then consider x being Element of dom f such that
A9: ( x = (len f) + 1 & x in dom f & f . x in e . x ) ;
(len f) + 1 <= len f by A9, FINSEQ_3:25;
hence contradiction by NAT_1:13; :: thesis: verum

end;

1 <= (len f) + 1 by NAT_1:11;
then ( (f ^ <*x*>) . ((len f) + 1) = x & (e ^ <*E*>) . ((len f) + 1) = E & (len f) + 1 in dom (f ^ <*x*>) ) by A1, A7, FINSEQ_3:25;
then (len f) + 1 in X1 by A2;
then {((len f) + 1)} c= X1 by ZFMISC_1:31;
then A10: X \/ {((len f) + 1)} c= X1 by A4, XBOOLE_1:8;
X1 c= X \/ {((len f) + 1)}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X1 or a in X \/ {((len f) + 1)} )
assume a in X1 ; :: thesis: a in X \/ {((len f) + 1)}
then consider y being Element of dom (f ^ <*x*>) such that
A11: ( y = a & y in dom (f ^ <*x*>) & (f ^ <*x*>) . y in (e ^ <*E*>) . y ) ;
reconsider y = y as Nat ;

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

suppose y = (len f) + 1 ; :: thesis: a in X \/ {((len f) + 1)}

hence a in X \/ {((len f) + 1)} by A11, ZFMISC_1:136; :: thesis: verum

end;

suppose A12: y <> (len f) + 1 ; :: thesis: a in X \/ {((len f) + 1)}

y <= (len f) + 1 by A7, FINSEQ_3:25;
then y < (len f) + 1 by A12, XXREAL_0:1;
then ( 1 <= y & y <= len f ) by NAT_1:13, FINSEQ_3:25;
then A13: 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;
then y in X by A11, A13;
hence a in X \/ {((len f) + 1)} by A11, ZFMISC_1:136; :: thesis: verum

end;

end;

end;

then X1 = X \/ {((len f) + 1)} by A10, XBOOLE_0:def 10;
then A14: card X1 = (card X) + 1 by A8, CARD_2:41;

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

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

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

end;

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

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

end;

end;