let f, g be Function of SCM-Memory,(Segm 2); :: thesis: ( ( for k being Element of SCM-Memory holds
( ( k = NAT implies f . k = 0 ) & ( k in SCM-Data-Loc implies f . k = 1 ) ) ) & ( for k being Element of SCM-Memory holds
( ( k = NAT implies g . k = 0 ) & ( k in SCM-Data-Loc implies g . k = 1 ) ) ) implies f = g )
assume that
A6: for k being Element of SCM-Memory holds
( ( k = NAT implies f . k = 0 ) & ( k in SCM-Data-Loc implies f . k = 1 ) ) and
A7: for k being Element of SCM-Memory holds
( ( k = NAT implies g . k = 0 ) & ( k in SCM-Data-Loc implies g . k = 1 ) ) ; :: thesis: f = g

now :: thesis: for k being Element of SCM-Memory holds f . k = g . k

let k be Element of SCM-Memory ; :: thesis: f . k = g . k

now :: thesis: f . k = g . k

per cases ( k = NAT or k in SCM-Data-Loc ) by Lm1;

suppose A8: k = NAT ; :: thesis: f . k = g . k

hence f . k = 0 by A6
.= g . k by A7, A8 ;
:: thesis: verum

end;

suppose A9: k in SCM-Data-Loc ; :: thesis: f . k = g . k

hence f . k = 1 by A6
.= g . k by A7, A9 ;
:: thesis: verum

end;

end;

end;

hence f . k = g . k ; :: thesis: verum

end;

hence f = g by FUNCT_2:63; :: thesis: verum