let f, g be Function of SCM-Memory ,({INT } \/ {SCMPDS-Instr ,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 ) & ( k in NAT implies f . k = SCMPDS-Instr ) ) ) & ( for k being Element of SCM-Memory holds
( ( k = NAT implies g . k = NAT ) & ( k in SCM-Data-Loc implies g . k = INT ) & ( k in NAT implies g . k = SCMPDS-Instr ) ) ) implies f = g )
assume that
A5: for k being Element of SCM-Memory holds
( ( k = NAT implies f . k = NAT ) & ( k in SCM-Data-Loc implies f . k = INT ) & ( k in NAT implies f . k = SCMPDS-Instr ) ) and
A6: for k being Element of SCM-Memory holds
( ( k = NAT implies g . k = NAT ) & ( k in SCM-Data-Loc implies g . k = INT ) & ( k in NAT implies g . k = SCMPDS-Instr ) ) ; :: 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 or k in NAT ) by Lm1;

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

hence f . k = NAT by A5
.= g . k by A6, A7 ;
:: thesis: verum

end;

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

hence f . k = INT by A5
.= g . k by A6, A8 ;
:: thesis: verum

end;

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

hence f . k = SCMPDS-Instr by A5
.= g . k by A6, A9 ;
:: thesis: verum

end;

end;

end;

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

end;

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