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 5;
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