defpred S₁[ Element of the carrier of I[01], Element of the carrier of I[01], set ] means ex a1, b1 being Point of (TOP-REAL n) st
( a1 = P . $1 & b1 = Q . $1 & $3 = ((1 - $2) * a1) + ($2 * b1) );
A1: for x, y being Element of the carrier of I[01] ex z being Element of T st S₁[x,y,z]

proof

let x, y be Element of the carrier of I[01]; :: thesis: ex z being Element of T st S₁[x,y,z]
A2: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1;
( P . x in the carrier of T & Q . x in the carrier of T ) ;
then reconsider a1 = P . x, b1 = Q . x as Point of (TOP-REAL n) by A2;
set z = ((1 - y) * a1) + (y * b1);
A3: y <= 1 by BORSUK_1:43;
[#] T is convex Subset of (TOP-REAL n) by Def1;
then A4: LSeg (a1,b1) c= [#] T by JORDAN1:def 1;
( y is Real & 0 <= y ) by BORSUK_1:43;
then ((1 - y) * a1) + (y * b1) in LSeg (a1,b1) by A3;
hence ex z being Element of T st S₁[x,y,z] by A4; :: thesis: verum

end;

consider F being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that
A5: for x, y being Element of the carrier of I[01] holds S₁[x,y,F . (x,y)] from BINOP_1:sch 3(A1);
reconsider F = F as Function of [:I[01],I[01]:],T by Lm1;
take F ; :: thesis: for s, t being Element of I[01]
for a1, b1 being Point of (TOP-REAL n) st a1 = P . s & b1 = Q . s holds
F . (s,t) = ((1 - t) * a1) + (t * b1)
let x, y be Element of the carrier of I[01]; :: thesis: for a1, b1 being Point of (TOP-REAL n) st a1 = P . x & b1 = Q . x holds
F . (x,y) = ((1 - y) * a1) + (y * b1)
ex a1, b1 being Point of (TOP-REAL n) st
( a1 = P . x & b1 = Q . x & F . (x,y) = ((1 - y) * a1) + (y * b1) ) by A5;
hence for a1, b1 being Point of (TOP-REAL n) st a1 = P . x & b1 = Q . x holds
F . (x,y) = ((1 - y) * a1) + (y * b1) ; :: thesis: verum