let x1, x2 be set ; :: thesis: for A being non empty set

for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( 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 = 1r ) ) ) holds

for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

let A be non empty set ; :: thesis: for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( 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 = 1r ) ) ) holds

for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

let f, g be Element of Funcs (A,COMPLEX); :: thesis: ( A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( 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 = 1r ) ) ) implies for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) )

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 = 1r ) & ( 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 = 1r ) ) ) ) ; :: thesis: for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

x2 in A by A1, TARSKI:def 2;

then A4: ( f . x2 = 0c & g . x2 = 1r ) by A2, A3;

x1 in A by A1, TARSKI:def 2;

then A5: ( f . x1 = 1r & g . x1 = 0c ) by A3;

let h be Element of Funcs (A,COMPLEX); :: thesis: ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult 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 Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

take b = h . x2; :: thesis: h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( 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 = 1r ) ) ) holds

for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

let A be non empty set ; :: thesis: for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( 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 = 1r ) ) ) holds

for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

let f, g be Element of Funcs (A,COMPLEX); :: thesis: ( A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( 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 = 1r ) ) ) implies for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) )

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 = 1r ) & ( 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 = 1r ) ) ) ) ; :: thesis: for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

x2 in A by A1, TARSKI:def 2;

then A4: ( f . x2 = 0c & g . x2 = 1r ) by A2, A3;

x1 in A by A1, TARSKI:def 2;

then A5: ( f . x1 = 1r & g . x1 = 0c ) by A3;

let h be Element of Funcs (A,COMPLEX); :: thesis: ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult 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 Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

take b = h . x2; :: thesis: h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

now :: thesis: for x being Element of A holds h . x = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x

hence
h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
by FUNCT_2:63; :: thesis: verumlet x be Element of A; :: thesis: h . x = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x

A6: ( x = x1 or x = x2 ) by A1, TARSKI:def 2;

A7: ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x2 = (((ComplexFuncExtMult A) . [a,f]) . x2) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th1

.= (a * (f . x2)) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th4

.= 0c + (b * 1r) by A4, Th4

.= h . x2 by COMPLEX1:def 4 ;

((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x1 = (((ComplexFuncExtMult A) . [a,f]) . x1) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th1

.= (a * (f . x1)) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th4

.= a + (b * 0c) by A5, Th4, COMPLEX1:def 4

.= h . x1 ;

hence h . x = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x by A6, A7; :: thesis: verum

end;A6: ( x = x1 or x = x2 ) by A1, TARSKI:def 2;

A7: ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x2 = (((ComplexFuncExtMult A) . [a,f]) . x2) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th1

.= (a * (f . x2)) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th4

.= 0c + (b * 1r) by A4, Th4

.= h . x2 by COMPLEX1:def 4 ;

((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x1 = (((ComplexFuncExtMult A) . [a,f]) . x1) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th1

.= (a * (f . x1)) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th4

.= a + (b * 0c) by A5, Th4, COMPLEX1:def 4

.= h . x1 ;

hence h . x = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x by A6, A7; :: thesis: verum