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:25;
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