let I be Element of Segm 15; for x being Element of SCMPDS-Instr
for k being Integer st x = [I,{},<*k*>] holds
x const_INT = k
let x be Element of SCMPDS-Instr ; for k being Integer st x = [I,{},<*k*>] holds
x const_INT = k
let k be Integer; ( x = [I,{},<*k*>] implies x const_INT = k )
assume A1:
x = [I,{},<*k*>]
; x const_INT = k
then consider f being FinSequence of INT such that
A2:
f = x `3_3
and
A3:
x const_INT = f /. 1
by Def3;
( k is Element of INT & f = <*k*> )
by A1, A2, INT_1:def 2;
hence
x const_INT = k
by A3, FINSEQ_4:16; verum