let N be non empty with_non-empty_elements set ; :: thesis: for I being Instruction of (STC N) holds AddressPart I = 0
let I be Instruction of (STC N); :: thesis: AddressPart I = 0
the Instructions of (STC N) = {[0 ,0 ],[1,0 ]} by AMISTD_1:def 11;
then ( I = [0 ,0 ] or I = [1,0 ] ) by TARSKI:def 2;
hence AddressPart I = 0 by MCART_1:def 2; :: thesis: verum