defpred S1[ 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 S1[x,y,z]
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 S1[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
; 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]; 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)
; verum