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 n
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 n
for x being Function of n,L holds eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
let b1, 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)
defpred S₁[ Element of NAT ] means for b1 being bag of n st card (support b1) = $1 holds
eval (b1 + b2),x = (eval b1,x) * (eval b2,x);
A1: ex k being Element of NAT st card (support b1) = k ;
A2: 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 A3: S₁[k] ; :: thesis: S₁[k + 1]
let b1 be bag of n; :: thesis: ( card (support b1) = k + 1 implies eval (b1 + b2),x = (eval b1,x) * (eval b2,x) )
assume A4: 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)));
A5: RelIncl n linearly_orders support b1 by Th15;
then SgmX (RelIncl n),(support b1) <> {} by A4, CARD_1:47, PRE_POLY:def 2, RELAT_1:60;
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 A6: 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 A6, FUNCT_1:def 5;
then A7: (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) in support b1 by A5, PRE_POLY:def 2;
set b19 = b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ;
support b1 c= dom b1 by PRE_POLY:37;
then A8: 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 A7, FUNCT_7:def 3;
A9: 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 A10: b1 . u <> 0 by PRE_POLY: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 A8, FUNCT_4:12;
then u in support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) by A10, PRE_POLY: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;

(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 A8, FUNCT_4:14;
then A11: (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 A12: 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 PRE_POLY:def 7;
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 A13: 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 A13, XBOOLE_0:def 3;

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

then u <> (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) by A11, PRE_POLY: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 A15: (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . u = b1 . u by A8, FUNCT_4:12;
(b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ) . u <> 0 by A14, PRE_POLY:def 7;
hence u in support b1 by A15, PRE_POLY: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 A7, 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 A9, TARSKI:2;
then A16: k + 1 = (card (support (b1 +* ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))),0 ))) + 1 by A4, A12, CARD_2:54;
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)))));
A17: dom b1 = n by PARTFUN1:def 4;
dom (EmptyBag n) = n by PARTFUN1:def 4;
then A18: (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 A7, FUNCT_7:def 3;
A19: 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 A20: ((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 PRE_POLY: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 A18, FUNCT_4:12;
hence contradiction by A20, PRE_POLY:52; :: thesis: verum

end;

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

end;

A21: b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) <> 0 by A7, PRE_POLY:def 7;
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)))))) )
(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 A18, FUNCT_4:14;
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)))))) . ((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;
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 u = (SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))) by TARSKI:def 1;
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 A21, A22, PRE_POLY:def 7; :: thesis: verum

end;

then A23: 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 A19, TARSKI:2;
A24: 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 A25: 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

(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 A18, FUNCT_4:14;
then A26: ((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;
u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by A25, TARSKI:def 1;
then u in dom (((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1)))) .--> 0 ) by FUNCOP_1:19;
then A27: (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 A8, A25, FUNCT_4:14;
((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 PRE_POLY:def 5
.= 0 + (b1 . ((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))) by A25, A27, A26, 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 A25; :: 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 A28: not u in {((SgmX (RelIncl n),(support b1)) /. (len (SgmX (RelIncl n),(support b1))))} by TARSKI:def 1;
then A29: 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 A28, 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 A18, FUNCT_4:12;
then A30: ((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 PRE_POLY:52;
((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 PRE_POLY:def 5
.= b1 . u by A8, A29, A30, 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;

A31: 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 by PARTFUN1:def 4;
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 A17, A24, 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 A23, 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 A3, A16
.= 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 A23, 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 PRE_POLY:35
.= eval (b1 + b2),x by A31, A17, A24, FUNCT_1:9 ;
:: thesis: verum

end;

A32: S₁[ 0 ]

proof

let b1 be bag of n; :: 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 A33: b1 = EmptyBag n by Th14;
hence eval (b1 + b2),x = eval b2,x by PRE_POLY:53
.= (1. L) * (eval b2,x) by VECTSP_1:def 16
.= (eval b1,x) * (eval b2,x) by A33, Th16 ;
:: thesis: verum

end;

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