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
A8: for s, t being Element of I[01] holds f . s,t = ((1 - t) * (P . s)) + (t * (Q . s)) and
A9: 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 A8
.= g . s,t by A9 ; :: thesis: verum

end;

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