let f, g be Function of [:F_{1}(),F_{2}():],F_{3}(); :: thesis: ( ( for s being Point of F_{1}()

for t being Point of F_{2}() holds f . (s,t) = F_{4}(s,t) ) & ( for s being Point of F_{1}()

for t being Point of F_{2}() holds g . (s,t) = F_{4}(s,t) ) implies f = g )

assume that

A1: for a being Point of F_{1}()

for b being Point of F_{2}() holds f . (a,b) = F_{4}(a,b)
and

A2: for a being Point of F_{1}()

for b being Point of F_{2}() holds g . (a,b) = F_{4}(a,b)
; :: thesis: f = g

let x be Point of [:F_{1}(),F_{2}():]; :: according to FUNCT_2:def 8 :: thesis: f . x = g . x

consider a being Point of F_{1}(), b being Point of F_{2}() such that

A3: x = [a,b] by BORSUK_1:10;

thus f . x = f . (a,b) by A3

.= F_{4}(a,b)
by A1

.= g . (a,b) by A2

.= g . x by A3 ; :: thesis: verum

for t being Point of F

for t being Point of F

assume that

A1: for a being Point of F

for b being Point of F

A2: for a being Point of F

for b being Point of F

let x be Point of [:F

consider a being Point of F

A3: x = [a,b] by BORSUK_1:10;

thus f . x = f . (a,b) by A3

.= F

.= g . (a,b) by A2

.= g . x by A3 ; :: thesis: verum