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 & 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 ; :: thesis: 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); :: thesis: ( 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) ) ; :: 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]))
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); :: thesis: 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; :: 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 :: thesis: for x being Element of A holds h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x

let x be Element of A; :: thesis: h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x
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 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; :: thesis: verum

end;

hence h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) by FUNCT_2:63; :: thesis: verum