let X be non empty set ; for x being Element of X
for c being non empty homogeneous quasi_total 2 -ary associative unital PartFunc of (X *),X st x is_a_unity_wrt c holds
for i being non empty homogeneous quasi_total 3 -ary PartFunc of (X *),X
for w being non empty homogeneous quasi_total 2 -ary PartFunc of (X *),X ex S being strict non-empty UAStr st
( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
let x be Element of X; for c being non empty homogeneous quasi_total 2 -ary associative unital PartFunc of (X *),X st x is_a_unity_wrt c holds
for i being non empty homogeneous quasi_total 3 -ary PartFunc of (X *),X
for w being non empty homogeneous quasi_total 2 -ary PartFunc of (X *),X ex S being strict non-empty UAStr st
( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
let c be non empty homogeneous quasi_total 2 -ary associative unital PartFunc of (X *),X; ( x is_a_unity_wrt c implies for i being non empty homogeneous quasi_total 3 -ary PartFunc of (X *),X
for w being non empty homogeneous quasi_total 2 -ary PartFunc of (X *),X ex S being strict non-empty UAStr st
( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial ) )
assume A1:
x is_a_unity_wrt c
; for i being non empty homogeneous quasi_total 3 -ary PartFunc of (X *),X
for w being non empty homogeneous quasi_total 2 -ary PartFunc of (X *),X ex S being strict non-empty UAStr st
( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
let i be non empty homogeneous quasi_total 3 -ary PartFunc of (X *),X; for w being non empty homogeneous quasi_total 2 -ary PartFunc of (X *),X ex S being strict non-empty UAStr st
( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
let w be non empty homogeneous quasi_total 2 -ary PartFunc of (X *),X; ex S being strict non-empty UAStr st
( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
set Y = 0 -tuples_on X;
set e = (0 -tuples_on X) --> x;
reconsider e = (0 -tuples_on X) --> x as non empty homogeneous quasi_total 0 -ary PartFunc of (X *),X ;
set char = <*e,c*> ^ <*i,w*>;
<*e,c*> ^ <*i,w*> is PFuncFinSequence of X
proof
let a be
object ;
TARSKI:def 3,
FINSEQ_1:def 4 ( a nin rng (<*e,c*> ^ <*i,w*>) or not a nin PFuncs ((X *),X) )
assume
a in rng (<*e,c*> ^ <*i,w*>)
;
not a nin PFuncs ((X *),X)
then
a in (rng <*e,c*>) \/ (rng <*i,w*>)
by FINSEQ_1:31;
then
(
a in rng <*e,c*> or
a in rng <*i,w*> )
by XBOOLE_0:def 3;
then
(
a in {e,c} or
a in {i,w} )
by FINSEQ_2:127;
then
(
a = e or
a = c or
a = i or
a = w )
by TARSKI:def 2;
hence
not
a nin PFuncs (
(X *),
X)
by PARTFUN1:45;
verum
end;
then reconsider char = <*e,c*> ^ <*i,w*> as non-empty non empty PFuncFinSequence of X ;
reconsider S = UAStr(# X,char #) as strict non-empty UAStr by UNIALG_1:def 3;
take
S
; ( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
thus
the carrier of S = X
; ( the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
thus
the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*>
; ( S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
A2:
len <*e,c*> = 2
by FINSEQ_1:44;
len <*i,w*> = 2
by FINSEQ_1:44;
then
len char = 2 + 2
by A2, FINSEQ_1:22;
then A3:
dom char = Seg 4
by FINSEQ_1:def 3;
reconsider e = e as non empty homogeneous 0 -ary PartFunc of ( the carrier of S *), the carrier of S ;
reconsider c = c as non empty homogeneous quasi_total 2 -ary associative PartFunc of ( the carrier of S *), the carrier of S ;
A4:
<*e,c*> . 1 = e
by FINSEQ_1:44;
A5:
<*e,c*> . 2 = c
by FINSEQ_1:44;
A6:
<*i,w*> . 1 = i
by FINSEQ_1:44;
A7:
<*i,w*> . 2 = w
by FINSEQ_1:44;
thus
1 in dom the charact of S
by A3; AOFA_000:def 10 ( the charact of S . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of S *), the carrier of S & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
A8:
dom <*e,c*> = Seg 2
by FINSEQ_1:89;
then A9:
1 in dom <*e,c*>
;
A10:
2 in dom <*e,c*>
by A8;
A11:
e = the charact of S . 1
by A4, A9, FINSEQ_1:def 7;
A12:
c = the charact of S . 2
by A5, A10, FINSEQ_1:def 7;
thus
the charact of S . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of S *), the carrier of S
by A4, A9, FINSEQ_1:def 7; ( S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
thus
2 in dom the charact of S
by A3; AOFA_000:def 11 ( the charact of S . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
thus
the charact of S . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S
by A5, A10, FINSEQ_1:def 7; ( S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
thus
S is unital
( S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )proof
take
c
;
AOFA_000:def 15 ( c = the charact of S . 2 & (Den ((In (1,(dom the charact of S))),S)) . {} is_a_unity_wrt c )
thus
c = the
charact of
S . 2
by A5, A10, FINSEQ_1:def 7;
(Den ((In (1,(dom the charact of S))),S)) . {} is_a_unity_wrt c
A13:
1
in dom the
charact of
S
by A3;
A14:
0 -tuples_on X = {{}}
by COMPUT_1:5;
A15:
In (1,
(dom the charact of S))
= 1
by A13, SUBSET_1:def 8;
A16:
{} in 0 -tuples_on X
by A14, TARSKI:def 1;
e = Den (
(In (1,(dom the charact of S))),
S)
by A4, A9, A15, FINSEQ_1:def 7;
hence
(Den ((In (1,(dom the charact of S))),S)) . {} is_a_unity_wrt c
by A1, A16, FUNCOP_1:7;
verum
end;
thus
the charact of S . 2 is non empty homogeneous quasi_total 2 -ary associative PartFunc of ( the carrier of S *), the carrier of S
by A5, A10, FINSEQ_1:def 7; AOFA_000:def 14 ( S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )
thus
3 in dom the charact of S
by A3; AOFA_000:def 12 ( the charact of S . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of S *), the carrier of S & S is with_while-instruction & S is quasi_total & S is partial )
A17:
dom <*i,w*> = Seg 2
by FINSEQ_1:89;
then A18:
1 in dom <*i,w*>
;
A19:
2 in dom <*i,w*>
by A17;
A20:
char . (2 + 1) = i
by A2, A6, A18, FINSEQ_1:def 7;
A21:
char . (2 + 2) = w
by A2, A7, A19, FINSEQ_1:def 7;
thus
the charact of S . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of S *), the carrier of S
by A20; ( S is with_while-instruction & S is quasi_total & S is partial )
thus
4 in dom the charact of S
by A3; AOFA_000:def 13 ( the charact of S . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S & S is quasi_total & S is partial )
thus
the charact of S . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S
by A2, A7, A19, FINSEQ_1:def 7; ( S is quasi_total & S is partial )
thus
S is quasi_total
S is partial
let i be Nat; UNIALG_1:def 1,MARGREL1:def 23 for b1 being Element of bool [:( the carrier of S *), the carrier of S:] holds
( not i in dom the charact of S or not b1 = the charact of S . i or b1 is homogeneous )
let h be PartFunc of ( the carrier of S *), the carrier of S; ( not i in dom the charact of S or not h = the charact of S . i or h is homogeneous )
assume that
A22:
i in dom the charact of S
and
A23:
h = the charact of S . i
; h is homogeneous
let p1, p2 be FinSequence; MARGREL1:def 1,MARGREL1:def 21 ( not p1 in dom h or not p2 in dom h or len p1 = len p2 )
( i = 1 or i = 2 or i = 3 or i = 4 )
by A3, A22, ENUMSET1:def 2, FINSEQ_3:2;
hence
( not p1 in dom h or not p2 in dom h or len p1 = len p2 )
by A11, A12, A20, A21, A23, MARGREL1:def 1; verum