let x1, x2 be set ; for A being non empty set
for f, g being Element of Funcs (A,REAL) st x1 in A & x2 in A & x1 <> x2 & f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) holds
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
let A be non empty set ; for f, g being Element of Funcs (A,REAL) st x1 in A & x2 in A & x1 <> x2 & f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) holds
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
let f, g be Element of Funcs (A,REAL); ( x1 in A & x2 in A & x1 <> x2 & f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) implies for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) )
assume that
A1:
x1 in A
and
A2:
x2 in A
and
A3:
x1 <> x2
and
A4:
( f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) )
; for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )
a5: f . x2 =
(RealFuncZero A) . x2
by A3, A4, FUNCT_4:83
.=
0
by A2, FUNCOP_1:7
;
A5: g . x2 =
(RealFuncUnit A) . x2
by A3, A4, FUNCT_4:83
.=
1
by A2, FUNCOP_1:7
;
a6:
f . x1 = 1
by A4, FUNCT_4:113;
A6:
g . x1 = 0
by A4, FUNCT_4:113;
let a, b be Real; ( (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A implies ( a = 0 & b = 0 ) )
reconsider x1 = x1, x2 = x2 as Element of A by A1, A2;
reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;
assume A7:
(RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A
; ( a = 0 & b = 0 )
then A8: 0 =
((RealFuncAdd A) . (((RealFuncExtMult A) . [aa,f]),((RealFuncExtMult A) . [bb,g]))) . x2
.=
(((RealFuncExtMult A) . [aa,f]) . x2) + (((RealFuncExtMult A) . [bb,g]) . x2)
by Th1
.=
(a * (f . x2)) + (((RealFuncExtMult A) . [bb,g]) . x2)
by Th4
.=
0 + (b * 1)
by A5, Th4, a5
.=
b
;
0 =
((RealFuncAdd A) . (((RealFuncExtMult A) . [aa,f]),((RealFuncExtMult A) . [bb,g]))) . x1
by A7
.=
(((RealFuncExtMult A) . [aa,f]) . x1) + (((RealFuncExtMult A) . [bb,g]) . x1)
by Th1
.=
(a * (f . x1)) + (((RealFuncExtMult A) . [bb,g]) . x1)
by Th4
.=
a + (b * 0)
by A6, Th4, a6
.=
a
;
hence
( a = 0 & b = 0 )
by A8; verum