let f, g be Action of (SCM-Instr R),(product ((SCM-VAL R) * SCM-OK)); :: thesis: ( ( for x being Element of SCM-Instr R
for y being SCM-State of R holds (f . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr R
for y being SCM-State of R holds (g . x) . y = SCM-Exec-Res (x,y) ) implies f = g )
assume that
A2: for x being Element of SCM-Instr R
for y being SCM-State of R holds (f . x) . y = SCM-Exec-Res (x,y) and
A3: for x being Element of SCM-Instr R
for y being SCM-State of R holds (g . x) . y = SCM-Exec-Res (x,y) ; :: thesis: f = g
now :: thesis: for x being Element of SCM-Instr R holds f . x = g . x
let x be Element of SCM-Instr R; :: thesis: f . x = g . x
reconsider gx = g . x, fx = f . x as Function of (product ((SCM-VAL R) * SCM-OK)),(product ((SCM-VAL R) * SCM-OK)) by FUNCT_2:66;
now :: thesis: for y being SCM-State of R holds fx . y = gx . y
let y be SCM-State of R; :: thesis: fx . y = gx . y
thus fx . y = SCM-Exec-Res (x,y) by A2
.= gx . y by A3 ; :: thesis: verum
end;
hence f . x = g . x by FUNCT_2:63; :: thesis: verum
end;
hence f = g by FUNCT_2:63; :: thesis: verum