let f, g be Function of [:I[01],I[01]:],T; :: thesis: ( ( 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)) ; :: thesis: f = g
for s, t being Element of the carrier of I[01] holds f . (s,t) = g . (s,t)

proof

let s, t be Element of the carrier of I[01]; :: thesis: f . (s,t) = g . (s,t)
thus f . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) by A9
.= g . (s,t) by A10 ; :: thesis: verum

end;

hence f = g by Lm1, BINOP_1:2; :: thesis: verum