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

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

hence
f = g
by FUNCT_2:63; :: thesis: verumlet k be Element of SCM-Memory ; :: thesis: f . k = g . k

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

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