let x1, x2 be set ; :: thesis: 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 ; :: thesis: 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); :: thesis: ( 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) ) ; :: thesis: 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; :: thesis: ( (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 ; :: thesis: ( 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; :: thesis: verum