let A be non empty set ; :: thesis: for f, g, h, f1 being Element of Funcs A,REAL
for x1, x2, x3, x4 being Element of A st x1 in A & x2 in A & x3 in A & x4 in A & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds
g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds
h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds
f1 . z = 0 ) holds
for a, b, c, d being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 & d = 0 )
let f, g, h, f1 be Element of Funcs A,REAL ; :: thesis: for x1, x2, x3, x4 being Element of A st x1 in A & x2 in A & x3 in A & x4 in A & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds
g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds
h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds
f1 . z = 0 ) holds
for a, b, c, d being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 & d = 0 )
let x1, x2, x3, x4 be Element of A; :: thesis: ( x1 in A & x2 in A & x3 in A & x4 in A & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds
g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds
h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds
f1 . z = 0 ) implies for a, b, c, d being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 & d = 0 ) )
set RM = RealFuncExtMult A;
set RA = RealFuncAdd A;
assume that
A1: ( x1 in A & x2 in A & x3 in A & x4 in A & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 ) and
A2: ( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) ) and
A3: ( g . x2 = 1 & ( for z being set st z in A & z <> x2 holds
g . z = 0 ) ) and
A4: ( h . x3 = 1 & ( for z being set st z in A & z <> x3 holds
h . z = 0 ) ) and
A5: ( f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds
f1 . z = 0 ) ) ; :: thesis: for a, b, c, d being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 & d = 0 )
A6: ( f . x1 = 1 & f . x2 = 0 & f . x3 = 0 & f . x4 = 0 & g . x1 = 0 & g . x2 = 1 & g . x3 = 0 & g . x4 = 0 & h . x1 = 0 & h . x2 = 0 & h . x3 = 1 & h . x4 = 0 & f1 . x1 = 0 & f1 . x2 = 0 & f1 . x3 = 0 & f1 . x4 = 1 ) by A1, A2, A3, A4, A5;
let a, b, c, d be Real; :: thesis: ( (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) = RealFuncZero A implies ( a = 0 & b = 0 & c = 0 & d = 0 ) )
assume A7: (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) = RealFuncZero A ; :: thesis: ( a = 0 & b = 0 & c = 0 & d = 0 )
then A8: 0 = ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1])) . x1 by FUNCOP_1:13
.= (((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])) . x1) + (((RealFuncExtMult A) . [d,f1]) . x1) by FUNCSDOM:10
.= ((((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x1) + (((RealFuncExtMult A) . [c,h]) . x1)) + (((RealFuncExtMult A) . [d,f1]) . x1) by FUNCSDOM:10
.= (((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (((RealFuncExtMult A) . [c,h]) . x1)) + (((RealFuncExtMult A) . [d,f1]) . x1) by FUNCSDOM:10
.= (((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (((RealFuncExtMult A) . [c,h]) . x1)) + (d * (f1 . x1)) by FUNCSDOM:15
.= (((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (c * (h . x1))) + (d * (f1 . x1)) by FUNCSDOM:15
.= (((((RealFuncExtMult A) . [a,f]) . x1) + (b * (g . x1))) + (c * (h . x1))) + (d * (f1 . x1)) by FUNCSDOM:15
.= (((a * 1) + (b * 0 )) + (c * 0 )) + (d * 0 ) by A6, FUNCSDOM:15
.= a ;
A9: 0 = ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1])) . x2 by A7, FUNCOP_1:13
.= (((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])) . x2) + (((RealFuncExtMult A) . [d,f1]) . x2) by FUNCSDOM:10
.= ((((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x2) + (((RealFuncExtMult A) . [c,h]) . x2)) + (((RealFuncExtMult A) . [d,f1]) . x2) by FUNCSDOM:10
.= (((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (((RealFuncExtMult A) . [c,h]) . x2)) + (((RealFuncExtMult A) . [d,f1]) . x2) by FUNCSDOM:10
.= (((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (((RealFuncExtMult A) . [c,h]) . x2)) + (d * (f1 . x2)) by FUNCSDOM:15
.= (((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (c * (h . x2))) + (d * (f1 . x2)) by FUNCSDOM:15
.= (((((RealFuncExtMult A) . [a,f]) . x2) + (b * (g . x2))) + (c * (h . x2))) + (d * (f1 . x2)) by FUNCSDOM:15
.= (((a * 0 ) + (b * 1)) + (c * 0 )) + (d * 0 ) by A6, FUNCSDOM:15
.= b ;
A10: 0 = ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1])) . x3 by A7, FUNCOP_1:13
.= (((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])) . x3) + (((RealFuncExtMult A) . [d,f1]) . x3) by FUNCSDOM:10
.= ((((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x3) + (((RealFuncExtMult A) . [c,h]) . x3)) + (((RealFuncExtMult A) . [d,f1]) . x3) by FUNCSDOM:10
.= (((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (((RealFuncExtMult A) . [c,h]) . x3)) + (((RealFuncExtMult A) . [d,f1]) . x3) by FUNCSDOM:10
.= (((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (((RealFuncExtMult A) . [c,h]) . x3)) + (d * (f1 . x3)) by FUNCSDOM:15
.= (((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (c * (h . x3))) + (d * (f1 . x3)) by FUNCSDOM:15
.= (((((RealFuncExtMult A) . [a,f]) . x3) + (b * (g . x3))) + (c * (h . x3))) + (d * (f1 . x3)) by FUNCSDOM:15
.= (((a * 0 ) + (b * 0 )) + (c * 1)) + (d * 0 ) by A6, FUNCSDOM:15
.= c ;
0 = ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1])) . x4 by A7, FUNCOP_1:13
.= (((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])) . x4) + (((RealFuncExtMult A) . [d,f1]) . x4) by FUNCSDOM:10
.= ((((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x4) + (((RealFuncExtMult A) . [c,h]) . x4)) + (((RealFuncExtMult A) . [d,f1]) . x4) by FUNCSDOM:10
.= (((((RealFuncExtMult A) . [a,f]) . x4) + (((RealFuncExtMult A) . [b,g]) . x4)) + (((RealFuncExtMult A) . [c,h]) . x4)) + (((RealFuncExtMult A) . [d,f1]) . x4) by FUNCSDOM:10
.= (((((RealFuncExtMult A) . [a,f]) . x4) + (((RealFuncExtMult A) . [b,g]) . x4)) + (((RealFuncExtMult A) . [c,h]) . x4)) + (d * (f1 . x4)) by FUNCSDOM:15
.= (((((RealFuncExtMult A) . [a,f]) . x4) + (((RealFuncExtMult A) . [b,g]) . x4)) + (c * (h . x4))) + (d * (f1 . x4)) by FUNCSDOM:15
.= (((((RealFuncExtMult A) . [a,f]) . x4) + (b * (g . x4))) + (c * (h . x4))) + (d * (f1 . x4)) by FUNCSDOM:15
.= (((a * 0 ) + (b * 0 )) + (c * 0 )) + (d * 1) by A6, FUNCSDOM:15
.= d ;
hence ( a = 0 & b = 0 & c = 0 & d = 0 ) by A8, A9, A10; :: thesis: verum