let A be non empty set ; for f, g, h, f1 being Element of Funcs (A,REAL)
for x1, x2, x3, x4 being Element of A st 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); for x1, x2, x3, x4 being Element of A st 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; ( 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 <> x2
and
A2:
x1 <> x3
and
A3:
x1 <> x4
and
A4:
x2 <> x3
and
A5:
x2 <> x4
and
A6:
x3 <> x4
and
A7:
f . x1 = 1
and
A8:
for z being set st z in A & z <> x1 holds
f . z = 0
and
A9:
g . x2 = 1
and
A10:
for z being set st z in A & z <> x2 holds
g . z = 0
and
A11:
h . x3 = 1
and
A12:
for z being set st z in A & z <> x3 holds
h . z = 0
and
A13:
f1 . x4 = 1
and
A14:
for z being set st z in A & z <> x4 holds
f1 . z = 0
; 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 )
A15:
( f . x2 = 0 & h . x2 = 0 )
by A1, A4, A8, A12;
A16:
( g . x1 = 0 & h . x1 = 0 )
by A1, A2, A10, A12;
A17:
f1 . x1 = 0
by A3, A14;
A18:
f1 . x2 = 0
by A5, A14;
let a, b, c, d be Real; ( (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 A19:
(RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) = RealFuncZero A
; ( a = 0 & b = 0 & c = 0 & d = 0 )
reconsider a = a, b = b, c = c, d = d as Element of REAL by XREAL_0:def 1;
A20: 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 FUNCOP_1:7, A19
.=
(((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x2) + (((RealFuncExtMult A) . [d,f1]) . x2)
by FUNCSDOM:1
.=
((((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x2) + (((RealFuncExtMult A) . [c,h]) . x2)) + (((RealFuncExtMult A) . [d,f1]) . x2)
by FUNCSDOM:1
.=
(((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (((RealFuncExtMult A) . [c,h]) . x2)) + (((RealFuncExtMult A) . [d,f1]) . x2)
by FUNCSDOM:1
.=
(((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (((RealFuncExtMult A) . [c,h]) . x2)) + (d * (f1 . x2))
by FUNCSDOM:4
.=
(((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (c * (h . x2))) + (d * (f1 . x2))
by FUNCSDOM:4
.=
(((((RealFuncExtMult A) . [a,f]) . x2) + (b * (g . x2))) + (c * (h . x2))) + (d * (f1 . x2))
by FUNCSDOM:4
.=
(((a * 0) + (b * 1)) + (c * 0)) + (d * 0)
by A9, A15, A18, FUNCSDOM:4
.=
b
;
A21:
( f . x4 = 0 & g . x4 = 0 )
by A3, A5, A8, A10;
A22:
h . x4 = 0
by A6, A12;
A23:
( f . x3 = 0 & g . x3 = 0 )
by A2, A4, A8, A10;
A24:
f1 . x3 = 0
by A6, A14;
A25: 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 A19, FUNCOP_1:7
.=
(((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x4) + (((RealFuncExtMult A) . [d,f1]) . x4)
by FUNCSDOM:1
.=
((((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x4) + (((RealFuncExtMult A) . [c,h]) . x4)) + (((RealFuncExtMult A) . [d,f1]) . x4)
by FUNCSDOM:1
.=
(((((RealFuncExtMult A) . [a,f]) . x4) + (((RealFuncExtMult A) . [b,g]) . x4)) + (((RealFuncExtMult A) . [c,h]) . x4)) + (((RealFuncExtMult A) . [d,f1]) . x4)
by FUNCSDOM:1
.=
(((((RealFuncExtMult A) . [a,f]) . x4) + (((RealFuncExtMult A) . [b,g]) . x4)) + (((RealFuncExtMult A) . [c,h]) . x4)) + (d * (f1 . x4))
by FUNCSDOM:4
.=
(((((RealFuncExtMult A) . [a,f]) . x4) + (((RealFuncExtMult A) . [b,g]) . x4)) + (c * (h . x4))) + (d * (f1 . x4))
by FUNCSDOM:4
.=
(((((RealFuncExtMult A) . [a,f]) . x4) + (b * (g . x4))) + (c * (h . x4))) + (d * (f1 . x4))
by FUNCSDOM:4
.=
(((a * 0) + (b * 0)) + (c * 0)) + (d * 1)
by A13, A21, A22, FUNCSDOM:4
.=
d
;
A26: 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 A19, FUNCOP_1:7
.=
(((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x3) + (((RealFuncExtMult A) . [d,f1]) . x3)
by FUNCSDOM:1
.=
((((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x3) + (((RealFuncExtMult A) . [c,h]) . x3)) + (((RealFuncExtMult A) . [d,f1]) . x3)
by FUNCSDOM:1
.=
(((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (((RealFuncExtMult A) . [c,h]) . x3)) + (((RealFuncExtMult A) . [d,f1]) . x3)
by FUNCSDOM:1
.=
(((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (((RealFuncExtMult A) . [c,h]) . x3)) + (d * (f1 . x3))
by FUNCSDOM:4
.=
(((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (c * (h . x3))) + (d * (f1 . x3))
by FUNCSDOM:4
.=
(((((RealFuncExtMult A) . [a,f]) . x3) + (b * (g . x3))) + (c * (h . x3))) + (d * (f1 . x3))
by FUNCSDOM:4
.=
(((a * 0) + (b * 0)) + (c * 1)) + (d * 0)
by A11, A23, A24, FUNCSDOM:4
.=
c
;
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 A19, FUNCOP_1:7
.=
(((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x1) + (((RealFuncExtMult A) . [d,f1]) . x1)
by FUNCSDOM:1
.=
((((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x1) + (((RealFuncExtMult A) . [c,h]) . x1)) + (((RealFuncExtMult A) . [d,f1]) . x1)
by FUNCSDOM:1
.=
(((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (((RealFuncExtMult A) . [c,h]) . x1)) + (((RealFuncExtMult A) . [d,f1]) . x1)
by FUNCSDOM:1
.=
(((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (((RealFuncExtMult A) . [c,h]) . x1)) + (d * (f1 . x1))
by FUNCSDOM:4
.=
(((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (c * (h . x1))) + (d * (f1 . x1))
by FUNCSDOM:4
.=
(((((RealFuncExtMult A) . [a,f]) . x1) + (b * (g . x1))) + (c * (h . x1))) + (d * (f1 . x1))
by FUNCSDOM:4
.=
(((a * 1) + (b * 0)) + (c * 0)) + (d * 0)
by A7, A16, A17, FUNCSDOM:4
.=
a
;
hence
( a = 0 & b = 0 & c = 0 & d = 0 )
by A20, A26, A25; verum