defpred S_{1}[ set , set ] means ( ( $1 = NAT & $2 = 0 ) or ( $1 in SCM-Data-Loc & $2 = 1 ) );

A5: for a being Element of SCM-Memory holds S_{1}[a,h . a]
from FUNCT_2:sch 3(A1);

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 A5, Lm2; :: thesis: ( k in SCM-Data-Loc implies h . k = 1 )

thus ( k in SCM-Data-Loc implies h . k = 1 ) by A5, Lm2; :: thesis: verum

thus verum ; :: thesis: verum

A1: now :: thesis: for k being Element of SCM-Memory ex b being Element of Segm 2 st S_{1}[k,b]

consider h being Function of SCM-Memory,(Segm 2) such that let k be Element of SCM-Memory ; :: thesis: ex b being Element of Segm 2 st S_{1}[k,b]

A2: {0} \/ {1} = {0,1} by ENUMSET1:1;

then A3: 0 in {1} \/ {0} by TARSKI:def 2;

A4: ( S_{1}[k, 0 ] or S_{1}[k,1] )
by Lm1;

1 in {1} \/ {0} by A2, TARSKI:def 2;

hence ex b being Element of Segm 2 st S_{1}[k,b]
by A2, A3, A4, CARD_1:50; :: thesis: verum

end;A2: {0} \/ {1} = {0,1} by ENUMSET1:1;

then A3: 0 in {1} \/ {0} by TARSKI:def 2;

A4: ( S

1 in {1} \/ {0} by A2, TARSKI:def 2;

hence ex b being Element of Segm 2 st S

A5: for a being Element of SCM-Memory holds S

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 A5, Lm2; :: thesis: ( k in SCM-Data-Loc implies h . k = 1 )

thus ( k in SCM-Data-Loc implies h . k = 1 ) by A5, Lm2; :: thesis: verum

thus verum ; :: thesis: verum