let T be InsType of {[0,{},{}],[1,{},{}]}; :: thesis: JumpParts T = {0}

set A = { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T } ;

{0} = { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T }

set A = { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T } ;

{0} = { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T }

proof

assume a in { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T } ; :: thesis: a in {0}

then consider I being Element of {[0,{},{}],[1,{},{}]} such that

A5: ( a = JumpPart I & InsCode I = T ) ;

( I = [0,{},{}] or I = [1,{},{}] ) by TARSKI:def 2;

then a = 0 by A5;

hence a in {0} by TARSKI:def 1; :: thesis: verum

end;

hence
JumpParts T = {0}
; :: thesis: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T } c= {0}

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T } or a in {0} )let a be object ; :: thesis: ( a in {0} implies a in { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T } )

assume a in {0} ; :: thesis: a in { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T }

then A1: a = 0 by TARSKI:def 1;

A2: ( InsCodes {[0,{},{}]} = {0} & InsCodes {[1,{},{}]} = {1} ) by MCART_1:92;

InsCodes {[0,{},{}],[1,{},{}]} = proj1_3 ({[0,{},{}]} \/ {[1,{},{}]}) by ENUMSET1:1

.= (InsCodes {[0,{},{}]}) \/ (InsCodes {[1,{},{}]}) by XTUPLE_0:31 ;

then ( T in {0} or T in {1} ) by A2, XBOOLE_0:def 3;

then A3: ( T = 0 or T = 1 ) by TARSKI:def 1;

reconsider I = [0,0,0], J = [1,0,0] as Element of {[0,{},{}],[1,{},{}]} by TARSKI:def 2;

A4: ( JumpPart I = 0 & JumpPart J = 0 ) ;

( InsCode I = 0 & InsCode J = 1 ) ;

hence a in { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T } by A1, A3, A4; :: thesis: verum

end;assume a in {0} ; :: thesis: a in { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T }

then A1: a = 0 by TARSKI:def 1;

A2: ( InsCodes {[0,{},{}]} = {0} & InsCodes {[1,{},{}]} = {1} ) by MCART_1:92;

InsCodes {[0,{},{}],[1,{},{}]} = proj1_3 ({[0,{},{}]} \/ {[1,{},{}]}) by ENUMSET1:1

.= (InsCodes {[0,{},{}]}) \/ (InsCodes {[1,{},{}]}) by XTUPLE_0:31 ;

then ( T in {0} or T in {1} ) by A2, XBOOLE_0:def 3;

then A3: ( T = 0 or T = 1 ) by TARSKI:def 1;

reconsider I = [0,0,0], J = [1,0,0] as Element of {[0,{},{}],[1,{},{}]} by TARSKI:def 2;

A4: ( JumpPart I = 0 & JumpPart J = 0 ) ;

( InsCode I = 0 & InsCode J = 1 ) ;

hence a in { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T } by A1, A3, A4; :: thesis: verum

assume a in { (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T } ; :: thesis: a in {0}

then consider I being Element of {[0,{},{}],[1,{},{}]} such that

A5: ( a = JumpPart I & InsCode I = T ) ;

( I = [0,{},{}] or I = [1,{},{}] ) by TARSKI:def 2;

then a = 0 by A5;

hence a in {0} by TARSKI:def 1; :: thesis: verum