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, b2 being bag of
for x being Function of n,L holds eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
let L be non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for b1, b2 being bag of
for x being Function of n,L holds eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
let b1, b2 be bag of ; :: 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)
defpred S₁[ Element of NAT ] means for b1 being bag of st card (support b1) = $1 holds
eval (b1 + b2),x = (eval b1,x) * (eval b2,x);
A1: S₁[ 0 ]

proof

let b1 be bag of ; :: thesis: ( card (support b1) = 0 implies eval (b1 + b2),x = (eval b1,x) * (eval b2,x) )
assume card (support b1) = 0 ; :: thesis: eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
then support b1 = {} ;
then A2: b1 = EmptyBag n by Th14;
hence eval (b1 + b2),x = eval b2,x by POLYNOM1:57
.= (1. L) * (eval b2,x) by VECTSP_1:def 16
.= (eval b1,x) * (eval b2,x) by A2, Th16 ;
:: thesis: verum

end;

A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let b1 be bag of ; :: thesis: ( card (support b1) = k + 1 implies eval (b1 + b2),x = (eval b1,x) * (eval b2,x) )
assume A5: card (support b1) = k + 1 ; :: thesis: eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
set sgb1 = SgmX (RelIncl n),(support b1);
set bg = (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)));
set b1' = b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ;
set m = (EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))));
A6: RelIncl n linearly_orders support b1 by Th15;
then rng (SgmX (RelIncl n),(support b1)) <> {} by A5, CARD_1:47, TRIANG_1:def 2;
then SgmX (RelIncl n),(support b1) <> {} by RELAT_1:60;
then len (SgmX (RelIncl n),(support b1)) <> 0 ;
then 1 <= len (SgmX (RelIncl n),(support b1)) by NAT_1:14;
then len (SgmX (RelIncl n),(support b1)) in Seg (len (SgmX (RelIncl n),(support b1))) by FINSEQ_1:3;
then A7: len (SgmX (RelIncl n),(support b1)) in dom (SgmX (RelIncl n),(support b1)) by FINSEQ_1:def 3;
then (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) = (SgmX (RelIncl n),(support b1)) . (len (SgmX (RelIncl n),(support b1))) by PARTFUN1:def 8;
then (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in rng (SgmX (RelIncl n),(support b1)) by A7, FUNCT_1:def 5;
then A8: (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in support b1 by A6, TRIANG_1:def 2;
then A9: b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) <> 0 by POLYNOM1:def 7;
A10: ( dom b1 = n & dom (EmptyBag n) = n ) by PARTFUN1:def 4;
support b1 c= dom b1 by POLYNOM1:41;
then A11: b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 = b1 +* (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> 0 ) by A8, FUNCT_7:def 3;
A12: (EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))) = (EmptyBag n) +* (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> (b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) by A8, A10, FUNCT_7:def 3;
(SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
then (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> 0 ) by FUNCOP_1:19;
then (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) = (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> 0 ) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) by A11, FUNCT_4:14;
then A13: (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) = 0 by FUNCOP_1:87;
then A14: not (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) by POLYNOM1:def 7;
A15: for u being set st u in support b1 holds
u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))}

proof

let u be set ; :: thesis: ( u in support b1 implies u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} )
assume u in support b1 ; :: thesis: u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))}
then A16: b1 . u <> 0 by POLYNOM1:def 7;

per cases ( u = (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) or u <> (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) ) ;

suppose u = (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) ; :: thesis: u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))}

then u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
hence u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose u <> (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) ; :: thesis: u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))}

then not u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
then not u in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> 0 ) by FUNCOP_1:19;
then (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . u = b1 . u by A11, FUNCT_4:12;
then u in support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) by A16, POLYNOM1:def 7;
hence u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

for u being set st u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} holds
u in support b1

proof

let u be set ; :: thesis: ( u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} implies u in support b1 )
assume A17: u in (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} ; :: thesis: u in support b1

per cases ( u in support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) or u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} ) by A17, XBOOLE_0:def 3;

suppose A18: u in support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) ; :: thesis: u in support b1

then A19: (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . u <> 0 by POLYNOM1:def 7;
u <> (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) by A13, A18, POLYNOM1:def 7;
then not u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
then not u in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> 0 ) by FUNCOP_1:19;
then (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . u = b1 . u by A11, FUNCT_4:12;
hence u in support b1 by A19, POLYNOM1:def 7; :: thesis: verum

end;

suppose u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} ; :: thesis: u in support b1

hence u in support b1 by A8, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then support b1 = (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )) \/ {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by A15, TARSKI:2;
then A20: k + 1 = (card (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ))) + 1 by A5, A14, CARD_2:54;
A21: for u being set st u in support ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) holds
u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))}

proof

let u be set ; :: thesis: ( u in support ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) implies u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} )
assume u in support ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) ; :: thesis: u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))}
then A22: ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . u <> 0 by POLYNOM1:def 7;

now

assume u <> (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) ; :: thesis: contradiction
then not u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
then not u in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> (b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) by FUNCOP_1:19;
then ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . u = (EmptyBag n) . u by A12, FUNCT_4:12;
hence contradiction by A22, POLYNOM1:56; :: thesis: verum

end;

hence u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1; :: thesis: verum

end;

for u being set st u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} holds
u in support ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))

proof

let u be set ; :: thesis: ( u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} implies u in support ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) )
assume u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} ; :: thesis: u in support ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))
then A23: u = (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) by TARSKI:def 1;
(SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
then (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> (b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) by FUNCOP_1:19;
then ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) = (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> (b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) by A12, FUNCT_4:14;
then ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) = b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) by FUNCOP_1:87;
hence u in support ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) by A9, A23, POLYNOM1:def 7; :: thesis: verum

end;

then A24: support ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) = {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by A21, TARSKI:2;
A25: ( dom ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) = n & dom b1 = n ) by PARTFUN1:def 4;
A26: for u being set st u in n holds
((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) . u = b1 . u

proof

let u be set ; :: thesis: ( u in n implies ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) . u = b1 . u )
assume u in n ; :: thesis: ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) . u = b1 . u

per cases ( u = (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) or u <> (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) ) ;

suppose A27: u = (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) ; :: thesis: ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) . u = b1 . u

then u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
then u in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> 0 ) by FUNCOP_1:19;
then A28: (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . u = (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> 0 ) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) by A11, A27, FUNCT_4:14;
(SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
then (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> (b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) by FUNCOP_1:19;
then ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) = (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> (b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) by A12, FUNCT_4:14;
then A29: ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) = b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) by FUNCOP_1:87;
((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) . u = ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . u) + (((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . u) by POLYNOM1:def 5
.= 0 + (b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))) by A27, A28, A29, FUNCOP_1:87
.= b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) ;
hence ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) . u = b1 . u by A27; :: thesis: verum

end;

suppose u <> (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) ; :: thesis: ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) . u = b1 . u

then A30: not u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
then A31: not u in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> 0 ) by FUNCOP_1:19;
not u in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> (b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) by A30, FUNCOP_1:19;
then ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . u = (EmptyBag n) . u by A12, FUNCT_4:12;
then A32: ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . u = 0 by POLYNOM1:56;
((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) . u = ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . u) + (((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) . u) by POLYNOM1:def 5
.= b1 . u by A11, A31, A32, FUNCT_4:12 ;
hence ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) . u = b1 . u ; :: thesis: verum

end;

end;

end;

then eval b1,x = eval (((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) + (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 )),x by A25, FUNCT_1:9
.= (eval (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ),x) * (eval ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))),x) by A24, Lm9 ;
hence (eval b1,x) * (eval b2,x) = ((eval (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ),x) * (eval b2,x)) * (eval ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))),x) by GROUP_1:def 4
.= (eval ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + b2),x) * (eval ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))),x) by A4, A20
.= eval (((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))))) + ((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + b2)),x by A24, Lm9
.= eval (((b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) + ((EmptyBag n) +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),(b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))))) + b2),x by POLYNOM1:39
.= eval (b1 + b2),x by A25, A26, FUNCT_1:9 ;
:: thesis: verum

end;

A33: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A3);
ex k being Element of NAT st card (support b1) = k ;
hence eval (b1 + b2),x = (eval b1,x) * (eval b2,x) by A33; :: thesis: verum