let n be Ordinal; :: thesis: for L being non empty non trivial well-unital doubleLoopStr
for u being set
for b being bag of st support b = {u} holds
for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u)
let L be non empty non trivial well-unital doubleLoopStr ; :: thesis: for u being set
for b being bag of st support b = {u} holds
for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u)
let u be set ; :: thesis: for b being bag of st support b = {u} holds
for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u)
let b be bag of ; :: thesis: ( support b = {u} implies for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u) )
assume A1:
support b = {u}
; :: thesis: for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u)
let x be Function of n,L; :: thesis: eval b,x = (power L) . (x . u),(b . u)
A2:
n = dom x
by FUNCT_2:def 1;
consider y being FinSequence of the carrier of L such that
A3:
( len y = len (SgmX (RelIncl n),(support b)) & eval b,x = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. i),((b * (SgmX (RelIncl n),(support b))) /. i) ) )
by Def2;
reconsider sb = support b as finite Subset of n ;
set sg = SgmX (RelIncl n),sb;
A4:
RelIncl n linearly_orders sb
by Th15;
then A5:
( rng (SgmX (RelIncl n),sb) = {u} & ( for l, m being Element of NAT st l in dom (SgmX (RelIncl n),sb) & m in dom (SgmX (RelIncl n),sb) & l < m holds
( (SgmX (RelIncl n),sb) /. l <> (SgmX (RelIncl n),sb) /. m & [((SgmX (RelIncl n),sb) /. l),((SgmX (RelIncl n),sb) /. m)] in RelIncl n ) ) )
by A1, TRIANG_1:def 2;
then A6:
u in rng (SgmX (RelIncl n),sb)
by TARSKI:def 1;
then A7:
1 in dom (SgmX (RelIncl n),sb)
by FINSEQ_3:33;
then A8:
for v being set st v in {1} holds
v in dom (SgmX (RelIncl n),sb)
by TARSKI:def 1;
for v being set st v in dom (SgmX (RelIncl n),sb) holds
v in {1}
proof
let v be
set ;
:: thesis: ( v in dom (SgmX (RelIncl n),sb) implies v in {1} )
assume A9:
v in dom (SgmX (RelIncl n),sb)
;
:: thesis: v in {1}
assume A10:
not
v in {1}
;
:: thesis: contradiction
reconsider v =
v as
Element of
NAT by A9;
A11:
v <> 1
by A10, TARSKI:def 1;
A12:
1
< v
(
(SgmX (RelIncl n),sb) /. 1
= (SgmX (RelIncl n),sb) . 1 &
(SgmX (RelIncl n),sb) /. v = (SgmX (RelIncl n),sb) . v )
by A6, A9, FINSEQ_3:33, PARTFUN1:def 8;
then A15:
(
(SgmX (RelIncl n),sb) /. 1
in rng (SgmX (RelIncl n),sb) &
(SgmX (RelIncl n),sb) /. v in rng (SgmX (RelIncl n),sb) )
by A7, A9, FUNCT_1:def 5;
then (SgmX (RelIncl n),sb) /. 1 =
u
by A5, TARSKI:def 1
.=
(SgmX (RelIncl n),sb) /. v
by A5, A15, TARSKI:def 1
;
hence
contradiction
by A4, A7, A9, A12, TRIANG_1:def 2;
:: thesis: verum
end;
then
dom (SgmX (RelIncl n),sb) = Seg 1
by A8, FINSEQ_1:4, TARSKI:2;
then A16:
len (SgmX (RelIncl n),sb) = 1
by FINSEQ_1:def 3;
then A17: y . 1 =
y /. 1
by A3, FINSEQ_4:24
.=
(power L) . ((x * (SgmX (RelIncl n),sb)) /. 1),((b * (SgmX (RelIncl n),sb)) /. 1)
by A3, A16
;
A18:
(SgmX (RelIncl n),sb) . 1 in rng (SgmX (RelIncl n),sb)
by A7, FUNCT_1:def 5;
then A19:
(SgmX (RelIncl n),sb) . 1 = u
by A5, TARSKI:def 1;
A20:
u in support b
by A1, TARSKI:def 1;
dom b = n
by PARTFUN1:def 4;
then
1 in dom (b * (SgmX (RelIncl n),sb))
by A7, A19, A20, FUNCT_1:21;
then A21: (b * (SgmX (RelIncl n),sb)) /. 1 =
(b * (SgmX (RelIncl n),sb)) . 1
by PARTFUN1:def 8
.=
b . ((SgmX (RelIncl n),sb) . 1)
by A7, FUNCT_1:23
.=
b . u
by A5, A18, TARSKI:def 1
;
A22:
x . u in rng x
by A2, A20, FUNCT_1:def 5;
rng x c= the carrier of L
by RELAT_1:def 19;
then reconsider xu = x . u as Element of L by A22;
A23:
(power L) . xu,(b . u) = (power L) . [xu,(b . u)]
;
1 in dom (x * (SgmX (RelIncl n),sb))
by A2, A7, A19, A20, FUNCT_1:21;
then (x * (SgmX (RelIncl n),sb)) /. 1 =
(x * (SgmX (RelIncl n),sb)) . 1
by PARTFUN1:def 8
.=
x . ((SgmX (RelIncl n),sb) . 1)
by A7, FUNCT_1:23
.=
x . u
by A5, A18, TARSKI:def 1
;
then
y = <*((power L) . (x . u),(b . u))*>
by A3, A16, A17, A21, FINSEQ_1:57;
hence
eval b,x = (power L) . (x . u),(b . u)
by A3, A23, GROUP_4:12; :: thesis: verum