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

for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & 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 a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0c & b = 0c )

let A be non empty set ; :: thesis: for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & 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 a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0c & b = 0c )

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

( a = 0c & b = 0c ) )

assume that

A1: x1 in A and

A2: x2 in A and

A3: x1 <> x2 and

A4: ( ( 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 a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0c & b = 0c )

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

A6: ( f . x1 = 1r & g . x1 = 0c ) by A1, A4;

let a, b be Complex; :: thesis: ( (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A implies ( a = 0c & b = 0c ) )

reconsider x1 = x1, x2 = x2 as Element of A by A1, A2;

assume A7: (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A ; :: thesis: ( a = 0c & b = 0c )

reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def 2;

A8: 0c = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x2 by FUNCOP_1:7, A7

.= (((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 A5, Th4

.= b by COMPLEX1:def 4 ;

0c = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x1 by A7, FUNCOP_1:7

.= (((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 A6, Th4, COMPLEX1:def 4

.= a ;

hence ( a = 0c & b = 0c ) by A8; :: thesis: verum

for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & 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 a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0c & b = 0c )

let A be non empty set ; :: thesis: for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & 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 a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0c & b = 0c )

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

( a = 0c & b = 0c ) )

assume that

A1: x1 in A and

A2: x2 in A and

A3: x1 <> x2 and

A4: ( ( 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 a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0c & b = 0c )

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

A6: ( f . x1 = 1r & g . x1 = 0c ) by A1, A4;

let a, b be Complex; :: thesis: ( (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A implies ( a = 0c & b = 0c ) )

reconsider x1 = x1, x2 = x2 as Element of A by A1, A2;

assume A7: (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A ; :: thesis: ( a = 0c & b = 0c )

reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def 2;

A8: 0c = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x2 by FUNCOP_1:7, A7

.= (((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 A5, Th4

.= b by COMPLEX1:def 4 ;

0c = ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))) . x1 by A7, FUNCOP_1:7

.= (((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 A6, Th4, COMPLEX1:def 4

.= a ;

hence ( a = 0c & b = 0c ) by A8; :: thesis: verum