let n be Ordinal; 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 ; 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; 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; 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;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
let b1 be
bag of
n;
( card (support b1) = k + 1 implies eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x)) )
assume A4:
card (support b1) = k + 1
;
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 ;
( 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
;
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))))
;
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;
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 ;
( 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)))))}
;
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))
;
u in support b1then
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;
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 ;
( 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))))))))
;
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 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))))
;
contradictionthen
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;
verum end;
hence
u in {((SgmX ((RelIncl n),(support b1))) /. (len (SgmX ((RelIncl n),(support b1)))))}
by TARSKI:def 1;
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 ;
( 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)))))}
;
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;
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 ;
( 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
;
((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))))
;
((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;
verum end; suppose
u <> (SgmX ((RelIncl n),(support b1))) /. (len (SgmX ((RelIncl n),(support b1))))
;
((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 . uthen 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
;
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
;
verum
end;
A32:
S1[ 0 ]
proof
let b1 be
bag of
n;
( card (support b1) = 0 implies eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x)) )
assume
card (support b1) = 0
;
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
;
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; verum