let f, g be Function of SCM-Memory,({INT} \/ {NAT}); :: thesis: ( ( for k being Element of SCM-Memory holds
( ( k = NAT implies f . k = NAT ) & ( k in SCM-Data-Loc implies f . k = INT ) ) ) & ( for k being Element of SCM-Memory holds
( ( k = NAT implies g . k = NAT ) & ( k in SCM-Data-Loc implies g . k = INT ) ) ) implies f = g )
assume that
A7: for k being Element of SCM-Memory holds
( ( k = NAT implies f . k = NAT ) & ( k in SCM-Data-Loc implies f . k = INT ) ) and
A8: for k being Element of SCM-Memory holds
( ( k = NAT implies g . k = NAT ) & ( k in SCM-Data-Loc implies g . k = INT ) ) ; :: thesis: f = g

now

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

now

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

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

hence f . k = NAT by A7
.= g . k by A8, A9 ;
:: thesis: verum

end;

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

hence f . k = INT by A7
.= g . k by A8, A10 ;
:: thesis: verum

end;

end;

end;

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

end;

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