let f, g be Function of [:I[01],I[01]:],T; ( ( for s, t being Element of I[01] holds f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds g . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) implies f = g )
assume that
A9:
for s, t being Element of I[01] holds f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
and
A10:
for s, t being Element of I[01] holds g . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
; f = g
for s, t being Element of the carrier of I[01] holds f . (s,t) = g . (s,t)
hence
f = g
by Lm1, BINOP_1:2; verum