let f, g be Function of SCM+FSA-Instr,(Funcs ((product (SCM*-VAL * SCM+FSA-OK)),(product (SCM*-VAL * SCM+FSA-OK)))); :: thesis: ( ( for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (f . x) . y = SCM+FSA-Exec-Res (x,y) ) & ( for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (g . x) . y = SCM+FSA-Exec-Res (x,y) ) implies f = g )

assume that

A2: for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (f . x) . y = SCM+FSA-Exec-Res (x,y) and

A3: for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (g . x) . y = SCM+FSA-Exec-Res (x,y) ; :: thesis: f = g

for y being SCM+FSA-State holds (f . x) . y = SCM+FSA-Exec-Res (x,y) ) & ( for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (g . x) . y = SCM+FSA-Exec-Res (x,y) ) implies f = g )

assume that

A2: for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (f . x) . y = SCM+FSA-Exec-Res (x,y) and

A3: for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (g . x) . y = SCM+FSA-Exec-Res (x,y) ; :: thesis: f = g

now :: thesis: for x being Element of SCM+FSA-Instr holds f . x = g . x

hence
f = g
by FUNCT_2:63; :: thesis: verumlet x be Element of SCM+FSA-Instr ; :: thesis: f . x = g . x

reconsider gx = g . x, fx = f . x as Function of (product (SCM*-VAL * SCM+FSA-OK)),(product (SCM*-VAL * SCM+FSA-OK)) ;

end;reconsider gx = g . x, fx = f . x as Function of (product (SCM*-VAL * SCM+FSA-OK)),(product (SCM*-VAL * SCM+FSA-OK)) ;

now :: thesis: for y being SCM+FSA-State holds fx . y = gx . y

hence
f . x = g . x
by FUNCT_2:63; :: thesis: verumlet y be SCM+FSA-State; :: thesis: fx . y = gx . y

thus fx . y = SCM+FSA-Exec-Res (x,y) by A2

.= gx . y by A3 ; :: thesis: verum

end;thus fx . y = SCM+FSA-Exec-Res (x,y) by A2

.= gx . y by A3 ; :: thesis: verum