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 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