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 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 S1[ 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 Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[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 PRE_POLY:82;
then SgmX ((RelIncl n),(support b1)) <> {} by A4, CARD_1:27, PRE_POLY:def 2, RELAT_1:38;
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:1;
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 6;
then (SgmX ((RelIncl n),(support b1))) /. (len (SgmX ((RelIncl n),(support b1)))) in rng (SgmX ((RelIncl n),(support b1))) by A6, FUNCT_1:def 3;
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 object 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 object ; :: 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) ;
then (b1 +* (((SgmX ((RelIncl n),(support b1))) /. (len (SgmX ((RelIncl n),(support b1))))),0)) . u = b1 . u by A8, FUNCT_4:11;
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) ;
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:13;
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:72;
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 object 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 object ; :: 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) ;
then A15: (b1 +* (((SgmX ((RelIncl n),(support b1))) /. (len (SgmX ((RelIncl n),(support b1))))),0)) . u = b1 . u by A8, FUNCT_4:11;
(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;
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:41;
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 2;
dom (EmptyBag n) = n by PARTFUN1:def 2;
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 object 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 object ; :: 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 :: thesis: not u <> (SgmX ((RelIncl n),(support b1))) /. (len (SgmX ((RelIncl n),(support b1))))
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))))))) ;
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:11;
hence contradiction by A20; :: 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 object 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 object ; :: 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))))))) ;
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:13;
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:72;
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 object 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 object ; :: 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))))))) ;
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:13;
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:72;
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) ;
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:13;
((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:72
.= 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) ;
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;
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:11;
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 ;
((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:11 ;
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 2;
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:2
.= (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, Lm5 ;
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 3
.= (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, Lm5
.= 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:2 ;
:: thesis: verum
end;
A32: S1[ 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 PRE_POLY:81;
hence eval ((b1 + b2),x) = (1. L) * (eval (b2,x)) by PRE_POLY:53
.= (eval (b1,x)) * (eval (b2,x)) by A33, Th6 ;
:: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A32, A2);
 hence eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x)) by A1; :: thesis: verum