let x1, x2 be set ; :: thesis: for A being non empty set
for f, g being Element of Funcs A,REAL st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) 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 ; :: thesis: for f, g being Element of Funcs A,REAL st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) 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 ; :: thesis: ( A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) 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} & x1 <> x2 )
and
A2:
for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) )
and
A3:
for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) )
; :: thesis: 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])
( x1 in A & x2 in A )
by A1, TARSKI:def 2;
then A4:
( f . x1 = 1 & f . x2 = 0 & g . x1 = 0 & g . x2 = 1 )
by A1, A2, A3;
reconsider x1 = x1, x2 = x2 as Element of A by A1, TARSKI:def 2;
let h be Element of Funcs A,REAL ; :: thesis: ex a, b being Real st h = (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])
take a = h . x1; :: thesis: ex b being Real st h = (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])
take b = h . x2; :: thesis: h = (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])
now let x be
Element of
A;
:: thesis: h . x = ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . xA5:
(
x = x1 or
x = x2 )
by A1, TARSKI:def 2;
A6:
((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x1 =
(((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)
by Th10
.=
(a * (f . x1)) + (((RealFuncExtMult A) . [b,g]) . x1)
by Th15
.=
a + (b * 0 )
by A4, Th15
.=
h . x1
;
((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x2 =
(((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)
by Th10
.=
(a * (f . x2)) + (((RealFuncExtMult A) . [b,g]) . x2)
by Th15
.=
0 + (b * 1)
by A4, Th15
.=
h . x2
;
hence
h . x = ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x
by A5, A6;
:: thesis: verum end;
hence
h = (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])
by FUNCT_2:113; :: thesis: verum