let f, g be Function of [:F₁(),F₂():],F₃(); :: thesis: ( ( for s being Point of F₁()
for t being Point of F₂() holds f . (s,t) = F₄(s,t) ) & ( for s being Point of F₁()
for t being Point of F₂() holds g . (s,t) = F₄(s,t) ) implies f = g )
assume that
A1: for a being Point of F₁()
for b being Point of F₂() holds f . (a,b) = F₄(a,b) and
A2: for a being Point of F₁()
for b being Point of F₂() holds g . (a,b) = F₄(a,b) ; :: thesis: f = g
let x be Point of [:F₁(),F₂():]; :: according to FUNCT_2:def 8 :: thesis: f . x = g . x
consider a being Point of F₁(), b being Point of F₂() such that
A3: x = [a,b] by BORSUK_1:10;
thus f . x = f . (a,b) by A3
.= F₄(a,b) by A1
.= g . (a,b) by A2
.= g . x by A3 ; :: thesis: verum