let x1, x2 be set ; for A being non empty set
for f, g being Element of Funcs (A,REAL) st A = {x1,x2} & x1 <> x2 & f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) holds
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
let A be non empty set ; for f, g being Element of Funcs (A,REAL) st A = {x1,x2} & x1 <> x2 & f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) holds
for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
let f, g be Element of Funcs (A,REAL); ( A = {x1,x2} & x1 <> x2 & f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) implies for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) )
assume that
A1:
A = {x1,x2}
and
A2:
x1 <> x2
and
A3:
( f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) )
; for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
a4:
x2 in A
by A1, TARSKI:def 2;
A4: f . x2 =
(RealFuncZero A) . x2
by A2, A3, FUNCT_4:83
.=
0
by FUNCOP_1:7, a4
;
A5: g . x2 =
(RealFuncUnit A) . x2
by A2, A3, FUNCT_4:83
.=
1
by FUNCOP_1:7, a4
;
a6:
f . x1 = 1
by A3, FUNCT_4:113;
B6:
g . x1 = 0
by A3, FUNCT_4:113;
let h be Element of Funcs (A,REAL); ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
reconsider x1 = x1, x2 = x2 as Element of A by A1, TARSKI:def 2;
take a = h . x1; ex b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
take b = h . x2; h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
now for x being Element of A holds h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . xlet x be
Element of
A;
h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . xA6:
(
x = x1 or
x = x2 )
by A1, TARSKI:def 2;
A7:
((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x2 =
(((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)
by Th1
.=
(a * (f . x2)) + (((RealFuncExtMult A) . [b,g]) . x2)
by Th4
.=
0 + (b * 1)
by A5, A4, Th4
.=
h . x2
;
((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x1 =
(((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)
by Th1
.=
(a * 1) + (((RealFuncExtMult A) . [b,g]) . x1)
by a6, Th4
.=
a + (b * 0)
by Th4, B6
.=
h . x1
;
hence
h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x
by A6, A7;
verum end;
hence
h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))
by FUNCT_2:63; verum