let S be COM-Struct ; :: thesis: for F being MacroInstruction of S st card F = 1 holds
F = Stop S
let F be MacroInstruction of S; :: thesis: ( card F = 1 implies F = Stop S )
assume A1: card F = 1 ; :: thesis: F = Stop S
then consider x being object such that
A2: F = {x} by CARD_2:42;
x in F by A2, TARSKI:def 1;
then consider a, b being object such that
A3: [a,b] = x by RELAT_1:def 1;
A4: dom F = {a} by A2, A3, RELAT_1:9;
A5: 0 in dom F by AFINSQ_1:65;
then A6: a = 0 by A4;
(card F) -' 1 = (card F) - 1 by PRE_CIRC:20
.= 0 by A1 ;
then LastLoc F = 0 by AFINSQ_1:70;
then F . 0 = halt S by Def6;
then halt S in rng F by A5, FUNCT_1:def 3;
then halt S in {b} by A2, A3, RELAT_1:9;
then F = {[0,(halt S)]} by A2, A3, A6, TARSKI:def 1
.= 0 .--> (halt S) by FUNCT_4:82 ;
hence F = Stop S ; :: thesis: verum