set I = the carrier of I[01] ;
let f, g be Function of [:I[01] ,I[01] :],(TOP-REAL n); :: 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
A2: for s, t being Element of I[01] holds f . s,t = ((1 - t) * (P . s)) + (t * (Q . s)) and
A3: for s, t being Element of I[01] holds g . s,t = ((1 - t) * (P . s)) + (t * (Q . s)) ; :: thesis: f = g
A4: 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 A2
.= g . s,t by A3 ; :: thesis: verum

end;

the carrier of [:I[01] ,I[01] :] = [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
hence f = g by A4, BINOP_1:2; :: thesis: verum