let f, g be Function of SCM-Instr ,(Funcs (product SCM-OK ),(product SCM-OK )); :: thesis: ( ( for x being Element of SCM-Instr
for y being SCM-State holds (f . x) . y = SCM-Exec-Res x,y ) & ( for x being Element of SCM-Instr
for y being SCM-State holds (g . x) . y = SCM-Exec-Res x,y ) implies f = g )
assume that
A2: for x being Element of SCM-Instr
for y being SCM-State holds (f . x) . y = SCM-Exec-Res x,y and
A3: for x being Element of SCM-Instr
for y being SCM-State holds (g . x) . y = SCM-Exec-Res x,y ; :: thesis: f = g

now

let x be Element of SCM-Instr ; :: thesis: f . x = g . x
reconsider gx = g . x, fx = f . x as Function of (product SCM-OK ),(product SCM-OK ) ;

now

let y be SCM-State; :: 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:113; :: thesis: verum

end;

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