let I be Element of Segm 14; :: thesis: 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 ; :: thesis: for k being Integer st x = [I,<*k*>] holds
x const_INT = k
let k be Integer; :: thesis: ( x = [I,<*k*>] implies x const_INT = k )
assume A1: x = [I,<*k*>] ; :: thesis: x const_INT = k
then consider f being FinSequence of INT such that
A2: ( f = x `2 & x const_INT = f /. 1 ) by Def11;
A3: k is Element of INT by INT_1:def 2;
f = <*k*> by A1, A2, MCART_1:7;
hence x const_INT = k by A2, A3, FINSEQ_4:25; :: thesis: verum