defpred S1[ set , set ] means ( ( \$1 = NAT & \$2 = 0 ) or ( \$1 in SCM-Data-Loc & \$2 = 1 ) );
A1: now :: thesis: for k being Element of SCM-Memory ex b being Element of Segm 2 st S1[k,b]
let k be Element of SCM-Memory ; :: thesis: ex b being Element of Segm 2 st S1[k,b]
A2: {0} \/ {1} = {0,1} by ENUMSET1:1;
then A3: 0 in {1} \/ by TARSKI:def 2;
A4: ( S1[k, 0 ] or S1[k,1] ) by Lm1;
1 in {1} \/ by ;
hence ex b being Element of Segm 2 st S1[k,b] by ; :: thesis: verum
end;
consider h being Function of SCM-Memory,(Segm 2) such that
A5: for a being Element of SCM-Memory holds S1[a,h . a] from take h ; :: thesis: for k being Element of SCM-Memory holds
( ( k = NAT implies h . k = 0 ) & ( k in SCM-Data-Loc implies h . k = 1 ) )

let k be Element of SCM-Memory ; :: thesis: ( ( k = NAT implies h . k = 0 ) & ( k in SCM-Data-Loc implies h . k = 1 ) )
thus ( k = NAT implies h . k = 0 ) by ; :: thesis: ( k in SCM-Data-Loc implies h . k = 1 )
thus ( k in SCM-Data-Loc implies h . k = 1 ) by ; :: thesis: verum
thus verum ; :: thesis: verum