let X be non empty set ; :: thesis: for x being Element of X
for c being non empty homogeneous quasi_total binary associative unital PartFunc of (X * ),X st x is_a_unity_wrt c holds
for i being non empty homogeneous quasi_total ternary PartFunc of (X * ),X
for w being non empty homogeneous quasi_total binary 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; :: thesis: for c being non empty homogeneous quasi_total binary associative unital PartFunc of (X * ),X st x is_a_unity_wrt c holds
for i being non empty homogeneous quasi_total ternary PartFunc of (X * ),X
for w being non empty homogeneous quasi_total binary 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 binary associative unital PartFunc of (X * ),X; :: thesis: ( x is_a_unity_wrt c implies for i being non empty homogeneous quasi_total ternary PartFunc of (X * ),X
for w being non empty homogeneous quasi_total binary 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
; :: thesis: for i being non empty homogeneous quasi_total ternary PartFunc of (X * ),X
for w being non empty homogeneous quasi_total binary 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 ternary PartFunc of (X * ),X; :: thesis: for w being non empty homogeneous quasi_total binary 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 binary PartFunc of (X * ),X; :: thesis: 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 nullary PartFunc of (X * ),X ;
set char = <*e,c*> ^ <*i,w*>;
reconsider ec = <*e,c*> as non empty FinSequence ;
<*e,c*> ^ <*i,w*> is PFuncFinSequence of X
proof
let a be
set ;
:: according to TARSKI:def 3,
FINSEQ_1:def 4 :: thesis: ( a nin proj2 (<*e,c*> ^ <*i,w*>) or not a nin PFuncs (X * ),X )
assume
a in rng (<*e,c*> ^ <*i,w*>)
;
:: thesis: not a nin PFuncs (X * ),X
then
a in (rng <*e,c*>) \/ (rng <*i,w*>)
by FINSEQ_1:44;
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:147;
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:119;
:: thesis: 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 9;
take
S
; :: thesis: ( 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
; :: thesis: ( 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*>
; :: thesis: ( 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 )
A3:
( len <*e,c*> = 2 & len <*i,w*> = 2 )
by FINSEQ_1:61;
then
len char = 2 + 2
by FINSEQ_1:35;
then A4:
dom char = Seg 4
by FINSEQ_1:def 3;
reconsider e = e as non empty homogeneous nullary PartFunc of (the carrier of S * ),the carrier of S ;
reconsider c = c as non empty homogeneous quasi_total binary associative PartFunc of (the carrier of S * ),the carrier of S ;
A5:
( <*e,c*> . 1 = e & <*e,c*> . 2 = c & <*i,w*> . 1 = i & <*i,w*> . 2 = w )
by FINSEQ_1:61;
thus
1 in dom the charact of S
by A4; :: according to AOFA_000:def 10 :: thesis: ( the charact of S . 1 is non empty homogeneous quasi_total nullary 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 )
dom <*e,c*> = Seg 2
by FINSEQ_3:29;
then A6:
( 1 in dom <*e,c*> & 2 in dom <*e,c*> )
;
then A7:
( e = the charact of S . 1 & c = the charact of S . 2 )
by A5, FINSEQ_1:def 7;
thus
the charact of S . 1 is non empty homogeneous quasi_total nullary PartFunc of (the carrier of S * ),the carrier of S
by A5, A6, FINSEQ_1:def 7; :: thesis: ( 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 A4; :: according to AOFA_000:def 11 :: thesis: ( the charact of S . 2 is non empty homogeneous quasi_total binary 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 binary PartFunc of (the carrier of S * ),the carrier of S
by A6, A5, FINSEQ_1:def 7; :: thesis: ( 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
:: thesis: ( S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )proof
take
c
;
:: according to AOFA_000:def 15 :: thesis: ( 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 A6, A5, FINSEQ_1:def 7;
:: thesis: (Den (In 1,(dom the charact of S)),S) . {} is_a_unity_wrt c
1
in dom the
charact of
S
by A4;
then
(
0 -tuples_on X = {{} } &
In 1,
(dom the charact of S) = 1 )
by COMPUT_1:8, FUNCT_7:def 1;
then
(
{} in 0 -tuples_on X &
e = Den (In 1,(dom the charact of S)),
S )
by A6, A5, FINSEQ_1:def 7, TARSKI:def 1;
hence
(Den (In 1,(dom the charact of S)),S) . {} is_a_unity_wrt c
by A1, FUNCOP_1:13;
:: thesis: verum
end;
thus
the charact of S . 2 is non empty homogeneous quasi_total binary associative PartFunc of (the carrier of S * ),the carrier of S
by A6, A5, FINSEQ_1:def 7; :: according to AOFA_000:def 14 :: thesis: ( 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 A4; :: according to AOFA_000:def 12 :: thesis: ( the charact of S . 3 is non empty homogeneous quasi_total ternary PartFunc of (the carrier of S * ),the carrier of S & S is with_while-instruction & S is quasi_total & S is partial )
dom <*i,w*> = Seg 2
by FINSEQ_3:29;
then
( 1 in dom <*i,w*> & 2 in dom <*i,w*> )
;
then A8:
( char . (2 + 1) = i & char . (2 + 2) = w )
by A3, A5, FINSEQ_1:def 7;
hence
the charact of S . 3 is non empty homogeneous quasi_total ternary PartFunc of (the carrier of S * ),the carrier of S
; :: thesis: ( S is with_while-instruction & S is quasi_total & S is partial )
thus
4 in dom the charact of S
by A4; :: according to AOFA_000:def 13 :: thesis: ( the charact of S . 4 is non empty homogeneous quasi_total binary 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 binary PartFunc of (the carrier of S * ),the carrier of S
by A8; :: thesis: ( S is quasi_total & S is partial )
thus
S is quasi_total
:: thesis: S is partial
let i be Nat; :: according to UNIALG_1:def 4,UNIALG_1:def 7 :: thesis: for b1 being Element of bool [:(the carrier of S * ),the carrier of S:] holds
( i nin 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; :: thesis: ( i nin dom the charact of S or not h = the charact of S . i or h is homogeneous )
assume A9:
( i in dom the charact of S & h = the charact of S . i )
; :: thesis: h is homogeneous
let p1, p2 be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( p1 nin proj1 h or p2 nin proj1 h or len p1 = len p2 )
( i = 1 or i = 2 or i = 3 or i = 4 )
by A4, A9, ENUMSET1:def 2, FINSEQ_3:2;
hence
( p1 nin proj1 h or p2 nin proj1 h or len p1 = len p2 )
by A7, A8, A9, UNIALG_1:def 1; :: thesis: verum