let T be InsType of ; :: thesis:
set A = { () where I is Element of : InsCode I = T } ;
{0} = { () where I is Element of : InsCode I = T }
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { () where I is Element of : InsCode I = T } c=
let a be object ; :: thesis: ( a in implies a in { () where I is Element of : InsCode I = T } )
assume a in ; :: thesis: a in { () where I is Element of : InsCode I = T }
then A1: a = 0 by TARSKI:def 1;
A2: InsCodes = by MCART_1:92;
A3: T = 0 by ;
reconsider I = [0,0,0] as Element of by TARSKI:def 1;
A4: JumpPart I = 0 ;
InsCode I = 0 ;
hence a in { () where I is Element of : InsCode I = T } by A1, A3, A4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { () where I is Element of : InsCode I = T } or a in )
assume a in { () where I is Element of : InsCode I = T } ; :: thesis:
then consider I being Element of such that
A5: ( a = JumpPart I & InsCode I = T ) ;
I = [0,{},{}] by TARSKI:def 1;
then a = 0 by A5;
hence a in by TARSKI:def 1; :: thesis: verum
end;
hence JumpParts T = ; :: thesis: verum