let T be InsType of SCM+FSA-Instr; :: according to COMPOS_0:def 7 :: thesis: for b_{1}, b_{2} being set holds

( not b_{1} in JumpParts T or not proj1 b_{1} = proj1 b_{2} or for b_{3} being object holds

( not [T,b_{1},b_{3}] in SCM+FSA-Instr or [T,b_{2},b_{3}] in SCM+FSA-Instr ) )

let f1, f2 be natural-valued Function; :: thesis: ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b_{1} being object holds

( not [T,f1,b_{1}] in SCM+FSA-Instr or [T,f2,b_{1}] in SCM+FSA-Instr ) )

assume that

A1: f1 in JumpParts T and

A2: dom f1 = dom f2 ; :: thesis: for b_{1} being object holds

( not [T,f1,b_{1}] in SCM+FSA-Instr or [T,f2,b_{1}] in SCM+FSA-Instr )

let p be object ; :: thesis: ( not [T,f1,p] in SCM+FSA-Instr or [T,f2,p] in SCM+FSA-Instr )

assume A3: [T,f1,p] in SCM+FSA-Instr ; :: thesis: [T,f2,p] in SCM+FSA-Instr

reconsider II = [T,f1,p] as Element of SCM+FSA-Instr by A3;

InsCode II <= 12 by Lm2;

then not not InsCode II = 0 & ... & not InsCode II = 12 by NAT_1:60;

( not b

( not [T,b

let f1, f2 be natural-valued Function; :: thesis: ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b

( not [T,f1,b

assume that

A1: f1 in JumpParts T and

A2: dom f1 = dom f2 ; :: thesis: for b

( not [T,f1,b

let p be object ; :: thesis: ( not [T,f1,p] in SCM+FSA-Instr or [T,f2,p] in SCM+FSA-Instr )

assume A3: [T,f1,p] in SCM+FSA-Instr ; :: thesis: [T,f2,p] in SCM+FSA-Instr

reconsider II = [T,f1,p] as Element of SCM+FSA-Instr by A3;

InsCode II <= 12 by Lm2;

then not not InsCode II = 0 & ... & not InsCode II = 12 by NAT_1:60;

per cases then
( InsCode II = 0 or InsCode II = 1 or InsCode II = 2 or InsCode II = 3 or InsCode II = 4 or InsCode II = 5 or InsCode II = 6 or InsCode II = 7 or InsCode II = 8 or T = 9 or T = 10 or T = 11 or T = 12 )
;

end;

suppose
( InsCode II = 0 or InsCode II = 1 or InsCode II = 2 or InsCode II = 3 or InsCode II = 4 or InsCode II = 5 or InsCode II = 6 or InsCode II = 7 or InsCode II = 8 )
; :: thesis: [T,f2,p] in SCM+FSA-Instr

then A4:
InsCode II <= 8
;

then reconsider ii = II as Element of SCM-Instr by Th2;

A5: T = InsCode ii ;

then T in InsCodes SCM-Instr ;

then reconsider t = T as InsType of SCM-Instr ;

A6: [t,f1,p] in SCM-Instr by A4, Th2;

JumpParts t = JumpParts T by A5, Lm5;

then [t,f2,p] in SCM-Instr by A1, A2, A6, COMPOS_0:def 7;

then [T,f2,p] in SCM-Instr ;

hence [T,f2,p] in SCM+FSA-Instr by Th1; :: thesis: verum

end;then reconsider ii = II as Element of SCM-Instr by Th2;

A5: T = InsCode ii ;

then T in InsCodes SCM-Instr ;

then reconsider t = T as InsType of SCM-Instr ;

A6: [t,f1,p] in SCM-Instr by A4, Th2;

JumpParts t = JumpParts T by A5, Lm5;

then [t,f2,p] in SCM-Instr by A1, A2, A6, COMPOS_0:def 7;

then [T,f2,p] in SCM-Instr ;

hence [T,f2,p] in SCM+FSA-Instr by Th1; :: thesis: verum