set I = the carrier of I[01];
deffunc H₁( Element of the carrier of I[01], Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL n) = ((1 - $2) * (P . $1)) + ($2 * (Q . $1));
consider F being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of (TOP-REAL n) such that
A1: for x, y being Element of the carrier of I[01] holds F . (x,y) = H₁(x,y) from BINOP_1:sch 4();
the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then reconsider F = F as Function of [:I[01],I[01]:],(TOP-REAL n) ;
take F ; :: thesis: for s, t being Element of I[01] holds F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
let x, y be Element of the carrier of I[01]; :: thesis: F . (x,y) = ((1 - y) * (P . x)) + (y * (Q . x))
thus F . (x,y) = ((1 - y) * (P . x)) + (y * (Q . x)) by A1; :: thesis: verum