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 2;
hence f = g by A4, BINOP_1:2; :: thesis: verum