let f, g be Function of [:I[01] ,I[01] :],T; :: 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) ) & ( 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
g . s,t = ((1 - t) * a1) + (t * b1) ) implies f = g )
assume that
A6: 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) and
A7: 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
g . s,t = ((1 - t) * a1) + (t * b1) ; :: thesis: f = g
for s, t being Element of the carrier of I[01] holds f . s,t = g . s,t

proof

let s, t be Element of the carrier of I[01] ; :: thesis: f . s,t = g . s,t
reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:55;
f . s,t = ((1 - t) * a1) + (t * b1) by A6;
hence f . s,t = g . s,t by A7; :: thesis: verum

end;

hence f = g by Lm1, BINOP_1:2; :: thesis: verum