let x1, x2 be set ; :: thesis:
let A be non empty set ; :: thesis:
let f, g be Element of Funcs (A,REAL); :: thesis:
assume that
A1: A = {x1,x2} and
A2: x1 <> x2 and
A3: ( ( 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 ) ) ) ) ; :: thesis:
x2 in A by A1, TARSKI:def 2;
then A4: ( f . x2 = 0 & g . x2 = 1 ) by A2, A3;
x1 in A by A1, TARSKI:def 2;
then A5: ( f . x1 = 1 & g . x1 = 0 ) by A3;
let h be Element of Funcs (A,REAL); :: thesis:
reconsider x1 = x1, x2 = x2 as Element of A by A1, TARSKI:def 2;
take a = h . x1; :: thesis:
take b = h . x2; :: thesis:

let x be Element of A; :: thesis:
A6: ( 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 Th10
.= (a * (f . x2)) + (((RealFuncExtMult A) . [b,g]) . x2) by Th15
.= 0 + (b * 1) by A4, Th15
.= h . x2 ;
((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 A5, Th15
.= h . x1 ;
hence h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x by A6, A7; :: thesis:

end;