let A be non empty set ; :: thesis: for f, g, h being Element of Funcs A,REAL
for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & 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 ) holds
for h' being Element of Funcs A,REAL ex a, b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
let f, g, h be Element of Funcs A,REAL ; :: thesis: for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & 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 ) holds
for h' being Element of Funcs A,REAL ex a, b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
let x1, x2, x3 be Element of A; :: thesis: ( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & 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 ) implies for h' being Element of Funcs A,REAL ex a, b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h]) )
assume that
A1:
( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )
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 ) )
; :: thesis: for h' being Element of Funcs A,REAL ex a, b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
A5:
( f . x1 = 1 & f . x2 = 0 & f . x3 = 0 & g . x1 = 0 & g . x2 = 1 & g . x3 = 0 & h . x1 = 0 & h . x2 = 0 & h . x3 = 1 )
by A1, A2, A3, A4;
let h' be Element of Funcs A,REAL ; :: thesis: ex a, b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
take a = h' . x1; :: thesis: ex b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
take b = h' . x2; :: thesis: ex c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
take c = h' . x3; :: thesis: h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
now let x be
Element of
A;
:: thesis: h' . x = ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])) . xA6:
(
x = x1 or
x = x2 or
x = x3 )
by A1, ENUMSET1:def 1;
A7:
((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])) . x1 =
(((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x1) + (((RealFuncExtMult A) . [c,h]) . x1)
by FUNCSDOM:10
.=
((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (((RealFuncExtMult A) . [c,h]) . x1)
by FUNCSDOM:10
.=
((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (c * (h . x1))
by FUNCSDOM:15
.=
((((RealFuncExtMult A) . [a,f]) . x1) + (b * (g . x1))) + (c * (h . x1))
by FUNCSDOM:15
.=
((a * 1) + (b * 0 )) + (c * 0 )
by A5, FUNCSDOM:15
.=
h' . x1
;
A8:
((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])) . x2 =
(((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x2) + (((RealFuncExtMult A) . [c,h]) . x2)
by FUNCSDOM:10
.=
((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (((RealFuncExtMult A) . [c,h]) . x2)
by FUNCSDOM:10
.=
((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (c * (h . x2))
by FUNCSDOM:15
.=
((((RealFuncExtMult A) . [a,f]) . x2) + (b * (g . x2))) + (c * (h . x2))
by FUNCSDOM:15
.=
((a * 0 ) + (b * 1)) + (c * 0 )
by A5, FUNCSDOM:15
.=
h' . x2
;
((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])) . x3 =
(((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x3) + (((RealFuncExtMult A) . [c,h]) . x3)
by FUNCSDOM:10
.=
((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (((RealFuncExtMult A) . [c,h]) . x3)
by FUNCSDOM:10
.=
((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (c * (h . x3))
by FUNCSDOM:15
.=
((((RealFuncExtMult A) . [a,f]) . x3) + (b * (g . x3))) + (c * (h . x3))
by FUNCSDOM:15
.=
((a * 0 ) + (b * 0 )) + (c * 1)
by A5, FUNCSDOM:15
.=
h' . x3
;
hence
h' . x = ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])) . x
by A6, A7, A8;
:: thesis: verum end;
hence
h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
by FUNCT_2:113; :: thesis: verum