defpred S1[ Element of the carrier of I[01], Element of the carrier of I[01], set ] means $3 = ((1 - $2) * (P . $1)) + ($2 * (Q . $1));
A1: for m, n being Element of the carrier of I[01] ex z being Element of T st S1[m,n,z]
proof
let m, n be Element of the carrier of I[01]; :: thesis: ex z being Element of T st S1[m,n,z]
A2: 0 <= n by BORSUK_1:43;
set z = ((1 - n) * (P . m)) + (n * (Q . m));
A3: n <= 1 by BORSUK_1:43;
per cases ( P . m <= Q . m or P . m > Q . m ) ;
suppose P . m <= Q . m ; :: thesis: ex z being Element of T st S1[m,n,z]
then ( P . m <= ((1 - n) * (P . m)) + (n * (Q . m)) & ((1 - n) * (P . m)) + (n * (Q . m)) <= Q . m ) by A2, A3, XREAL_1:172, XREAL_1:173;
then A4: ((1 - n) * (P . m)) + (n * (Q . m)) in [.(P . m),(Q . m).] by XXREAL_1:1;
[.(P . m),(Q . m).] c= the carrier of T by Th8;
hence ex z being Element of T st S1[m,n,z] by A4; :: thesis: verum
end;
suppose A5: P . m > Q . m ; :: thesis: ex z being Element of T st S1[m,n,z]
1 - 1 <= 1 - n by A3, XREAL_1:13;
then (1 - n) * (Q . m) <= (1 - n) * (P . m) by A5, XREAL_1:64;
then A6: ((1 - n) * (Q . m)) + (n * (Q . m)) <= ((1 - n) * (P . m)) + (n * (Q . m)) by XREAL_1:6;
A7: [.(Q . m),(P . m).] c= the carrier of T by Th8;
(Q . m) - (P . m) < (Q . m) - (Q . m) by A5, XREAL_1:15;
then n * ((Q . m) - (P . m)) <= n * 0 by A2, XREAL_1:131;
then (P . m) + (n * ((Q . m) - (P . m))) <= (P . m) + 0 by XREAL_1:6;
then ((1 - n) * (P . m)) + (n * (Q . m)) in [.(Q . m),(P . m).] by A6, XXREAL_1:1;
hence ex z being Element of T st S1[m,n,z] by A7; :: thesis: verum
end;
end;
end;
consider F being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that
A8: for m, n being Element of the carrier of I[01] holds S1[m,n,F . (m,n)] 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] holds F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
let s, t be Element of the carrier of I[01]; :: thesis: F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
thus F . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) by A8; :: thesis: verum