let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for b1 being bag of n st ex u being set st support b1 = {u} holds
for b2 being bag of n
for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))
let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for b1 being bag of n st ex u being set st support b1 = {u} holds
for b2 being bag of n
for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))
let b1 be bag of n; :: thesis: ( ex u being set st support b1 = {u} implies for b2 being bag of n
for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x)) )
assume ex u being set st support b1 = {u} ; :: thesis: for b2 being bag of n
for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))
then consider u being set such that
A1: support b1 = {u} ;
let b2 be bag of n; :: thesis: for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))
let x be Function of n,L; :: thesis: eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))
A2: support (b1 + b2) = (support b2) \/ {u} by A1, PRE_POLY:38;
A3: for u9 being object st u9 <> u holds
(b1 + b2) . u9 = b2 . u9
proof
let u9 be object ; :: thesis: ( u9 <> u implies (b1 + b2) . u9 = b2 . u9 )
assume u9 <> u ; :: thesis: (b1 + b2) . u9 = b2 . u9
then A4: not u9 in support b1 by A1, TARSKI:def 1;
thus (b1 + b2) . u9 = (b1 . u9) + (b2 . u9) by PRE_POLY:def 5
.= 0 + (b2 . u9) by A4, PRE_POLY:def 7
.= b2 . u9 ; :: thesis: verum
end;
set sb2 = SgmX ((RelIncl n),(support b2));
set sb1b2 = SgmX ((RelIncl n),(support (b1 + b2)));
A5: n c= dom x by FUNCT_2:def 1;
A6: RelIncl n linearly_orders support b2 by PRE_POLY:82;
consider yb1b2 being FinSequence of the carrier of L such that
A7: len yb1b2 = len (SgmX ((RelIncl n),(support (b1 + b2)))) and
A8: eval ((b1 + b2),x) = Product yb1b2 and
A9: for i being Element of NAT st 1 <= i & i <= len yb1b2 holds
yb1b2 /. i = (power L) . (((x * (SgmX ((RelIncl n),(support (b1 + b2))))) /. i),(((b1 + b2) * (SgmX ((RelIncl n),(support (b1 + b2))))) /. i)) by Def1;
consider yb2 being FinSequence of the carrier of L such that
A10: len yb2 = len (SgmX ((RelIncl n),(support b2))) and
A11: eval (b2,x) = Product yb2 and
A12: for i being Element of NAT st 1 <= i & i <= len yb2 holds
yb2 /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b2)))) /. i),((b2 * (SgmX ((RelIncl n),(support b2)))) /. i)) by Def1;
per cases ( u in support b2 or not u in support b2 ) ;
suppose A13: u in support b2 ; :: thesis: eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))
consider sb2k being Nat such that
A14: dom (SgmX ((RelIncl n),(support b2))) = Seg sb2k by FINSEQ_1:def 2;
A15: for v being object st v in support b2 holds
v in support (b1 + b2)
proof
let v be object ; :: thesis: ( v in support b2 implies v in support (b1 + b2) )
assume A16: v in support b2 ; :: thesis: v in support (b1 + b2)
now :: thesis: ( ( u = v & v in support (b1 + b2) ) or ( u <> v & v in support (b1 + b2) ) )
per cases ( u = v or u <> v ) ;
case u <> v ; :: thesis: v in support (b1 + b2)
then (b1 + b2) . v = b2 . v by A3;
then (b1 + b2) . v <> 0 by A16, PRE_POLY:def 7;
hence v in support (b1 + b2) by PRE_POLY:def 7; :: thesis: verum
end;
end;
end;
hence v in support (b1 + b2) ; :: thesis: verum
end;
A17: for v being object st v in support (b1 + b2) holds
v in support b2
proof
let v be object ; :: thesis: ( v in support (b1 + b2) implies v in support b2 )
assume A18: v in support (b1 + b2) ; :: thesis: v in support b2
hence v in support b2 ; :: thesis: verum
end;
then A19: len yb1b2 = len yb2 by A7, A10, A15, TARSKI:2;
A20: support (b1 + b2) = support b2 by A17, A15, TARSKI:2;
u in rng (SgmX ((RelIncl n),(support b2))) by A6, A13, PRE_POLY:def 2;
then consider k being Nat such that
A21: k in dom (SgmX ((RelIncl n),(support b2))) and
A22: (SgmX ((RelIncl n),(support b2))) . k = u by FINSEQ_2:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A23: 1 <= k by A21, A14, FINSEQ_1:1;
A24: support b2 c= dom b2 by PRE_POLY:37;
then A25: k in dom (b2 * (SgmX ((RelIncl n),(support b2)))) by A13, A21, A22, FUNCT_1:11;
then (b2 * (SgmX ((RelIncl n),(support b2)))) /. k = (b2 * (SgmX ((RelIncl n),(support b2)))) . k by PARTFUN1:def 6;
then A26: (b2 * (SgmX ((RelIncl n),(support b2)))) /. k = b2 . u by A22, A25, FUNCT_1:12;
A27: rng x c= the carrier of L by RELAT_1:def 19;
consider sb1b2k being Nat such that
A28: dom (SgmX ((RelIncl n),(support (b1 + b2)))) = Seg sb1b2k by FINSEQ_1:def 2;
support (b1 + b2) c= dom (b1 + b2) by PRE_POLY:37;
then A29: k in dom ((b1 + b2) * (SgmX ((RelIncl n),(support b2)))) by A13, A20, A21, A22, FUNCT_1:11;
then A30: ((b1 + b2) * (SgmX ((RelIncl n),(support b2)))) /. k = ((b1 + b2) * (SgmX ((RelIncl n),(support b2)))) . k by PARTFUN1:def 6
.= (b1 + b2) . u by A22, A29, FUNCT_1:12 ;
consider i being Nat such that
A31: dom yb2 = Seg i by FINSEQ_1:def 2;
reconsider sb2k = sb2k, sb1b2k = sb1b2k as Element of NAT by ORDINAL1:def 12;
A32: k <= sb2k by A21, A14, FINSEQ_1:1;
i in NAT by ORDINAL1:def 12;
then A33: len yb2 = i by A31, FINSEQ_1:def 3;
A34: sb2k = len yb2 by A10, A14, FINSEQ_1:def 3;
then A35: k in dom yb2 by A21, A14, FINSEQ_1:def 3;
reconsider bbS = b2 * (SgmX ((RelIncl n),(support b2))) as PartFunc of NAT,NAT ;
A36: sb2k = len (SgmX ((RelIncl n),(support b2))) by A14, FINSEQ_1:def 3
.= len (SgmX ((RelIncl n),(support (b1 + b2)))) by A17, A15, TARSKI:2
.= sb1b2k by A28, FINSEQ_1:def 3 ;
then len yb1b2 = sb2k by A7, A28, FINSEQ_1:def 3;
then A37: yb1b2 /. k = (power L) . (((x * (SgmX ((RelIncl n),(support b2)))) /. k),(((b1 + b2) * (SgmX ((RelIncl n),(support b2)))) /. k)) by A9, A20, A23, A32
.= (power L) . (((x * (SgmX ((RelIncl n),(support b2)))) /. k),((b1 . u) + (b2 . u))) by A30, PRE_POLY:def 5
.= ((power L) . (((x * (SgmX ((RelIncl n),(support b2)))) /. k),(b1 . u))) * ((power L) . (((x * (SgmX ((RelIncl n),(support b2)))) /. k),(bbS /. k))) by A26, Th1
.= ((power L) . (((x * (SgmX ((RelIncl n),(support b2)))) /. k),(b1 . u))) * (yb2 /. k) by A12, A23, A32, A34 ;
A38: dom (b1 + b2) = n by PARTFUN1:def 2;
A39: for i9 being Element of NAT st i9 in dom yb2 & i9 <> k holds
yb1b2 /. i9 = yb2 /. i9
proof
rng (SgmX ((RelIncl n),(support (b1 + b2)))) c= dom b2 by A6, A20, A24, PRE_POLY:def 2;
then A40: rng (SgmX ((RelIncl n),(support (b1 + b2)))) c= n by PARTFUN1:def 2;
A41: rng (SgmX ((RelIncl n),(support b2))) c= dom b2 by A6, A24, PRE_POLY:def 2;
let i9 be Element of NAT ; :: thesis: ( i9 in dom yb2 & i9 <> k implies yb1b2 /. i9 = yb2 /. i9 )
assume that
A42: i9 in dom yb2 and
A43: i9 <> k ; :: thesis: yb1b2 /. i9 = yb2 /. i9
A44: 1 <= i9 by A31, A42, FINSEQ_1:1;
A45: i9 in dom (SgmX ((RelIncl n),(support b2))) by A10, A31, A33, A42, FINSEQ_1:def 3;
then (SgmX ((RelIncl n),(support b2))) . i9 in rng (SgmX ((RelIncl n),(support b2))) by FUNCT_1:def 3;
then A46: i9 in dom (b2 * (SgmX ((RelIncl n),(support b2)))) by A45, A41, FUNCT_1:11;
then A47: (b2 * (SgmX ((RelIncl n),(support b2)))) /. i9 = (b2 * (SgmX ((RelIncl n),(support b2)))) . i9 by PARTFUN1:def 6
.= b2 . ((SgmX ((RelIncl n),(support b2))) . i9) by A46, FUNCT_1:12
.= b2 . ((SgmX ((RelIncl n),(support b2))) /. i9) by A45, PARTFUN1:def 6 ;
A48: i9 <= len yb2 by A31, A33, A42, FINSEQ_1:1;
A49: i9 in Seg sb1b2k by A36, A34, A42, FINSEQ_1:def 3;
A50: (SgmX ((RelIncl n),(support (b1 + b2)))) /. i9 <> u
proof
assume (SgmX ((RelIncl n),(support (b1 + b2)))) /. i9 = u ; :: thesis: contradiction
then A51: (SgmX ((RelIncl n),(support (b1 + b2)))) . i9 = u by A28, A49, PARTFUN1:def 6;
A52: SgmX ((RelIncl n),(support (b1 + b2))) is one-to-one by PRE_POLY:10, PRE_POLY:82;
(SgmX ((RelIncl n),(support (b1 + b2)))) . k = u by A17, A15, A22, TARSKI:2;
hence contradiction by A21, A14, A28, A36, A43, A49, A51, A52, FUNCT_1:def 4; :: thesis: verum
end;
(SgmX ((RelIncl n),(support (b1 + b2)))) . i9 in rng (SgmX ((RelIncl n),(support (b1 + b2)))) by A28, A49, FUNCT_1:def 3;
then A53: i9 in dom ((b1 + b2) * (SgmX ((RelIncl n),(support (b1 + b2))))) by A28, A38, A49, A40, FUNCT_1:11;
then ((b1 + b2) * (SgmX ((RelIncl n),(support (b1 + b2))))) /. i9 = ((b1 + b2) * (SgmX ((RelIncl n),(support (b1 + b2))))) . i9 by PARTFUN1:def 6
.= (b1 + b2) . ((SgmX ((RelIncl n),(support (b1 + b2)))) . i9) by A53, FUNCT_1:12
.= (b1 + b2) . ((SgmX ((RelIncl n),(support (b1 + b2)))) /. i9) by A28, A49, PARTFUN1:def 6 ;
hence yb1b2 /. i9 = (power L) . (((x * (SgmX ((RelIncl n),(support (b1 + b2))))) /. i9),((b1 + b2) . ((SgmX ((RelIncl n),(support (b1 + b2)))) /. i9))) by A9, A19, A44, A48
.= (power L) . (((x * (SgmX ((RelIncl n),(support b2)))) /. i9),(b2 . ((SgmX ((RelIncl n),(support b2))) /. i9))) by A3, A20, A50
.= yb2 /. i9 by A12, A44, A48, A47 ;
:: thesis: verum
end;
A54: support b1 c= dom b1 by PRE_POLY:37;
u in support b1 by A1, TARSKI:def 1;
then A55: u in dom b1 by A54;
A56: dom b1 = n by PARTFUN1:def 2;
then x . u in rng x by A5, A55, FUNCT_1:def 3;
then reconsider xu = x . u as Element of L by A27;
consider a being Element of L such that
A57: a = (power L) . (xu,(b1 . u)) ;
A58: k in dom (x * (SgmX ((RelIncl n),(support b2)))) by A5, A21, A22, A55, A56, FUNCT_1:11;
then (x * (SgmX ((RelIncl n),(support b2)))) . k = x . ((SgmX ((RelIncl n),(support b2))) . k) by FUNCT_1:12;
then yb1b2 /. k = a * (yb2 /. k) by A22, A37, A57, A58, PARTFUN1:def 6;
hence eval ((b1 + b2),x) = a * (Product yb2) by A8, A19, A35, A39, Th5
.= (eval (b1,x)) * (eval (b2,x)) by A1, A11, A57, Th7 ;
:: thesis: verum
end;
suppose A59: not u in support b2 ; :: thesis: eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))
A60: support b1 c= dom b1 by PRE_POLY:37;
u in support b1 by A1, TARSKI:def 1;
then A61: u in dom b1 by A60;
A62: rng x c= the carrier of L by RELAT_1:def 19;
dom b1 = n by PARTFUN1:def 2;
then x . u in rng x by A5, A61, FUNCT_1:def 3;
then reconsider xu = x . u as Element of L by A62;
consider a being Element of L such that
A63: a = (power L) . (xu,((b1 + b2) . u)) ;
A64: (b1 + b2) . u = (b1 . u) + (b2 . u) by PRE_POLY:def 5
.= (b1 . u) + 0 by A59, PRE_POLY:def 7 ;
thus eval ((b1 + b2),x) = a * (eval (b2,x)) by A3, A2, A59, A63, Lm4
.= (eval (b1,x)) * (eval (b2,x)) by A1, A64, A63, Th7 ; :: thesis: verum
end;
end;