let X be non empty set ; :: thesis:
let x be Element of X; :: thesis:
let c be non empty homogeneous quasi_total 2 -ary associative unital PartFunc of (X *),X; :: thesis:
assume A1: x is_a_unity_wrt c ; :: thesis:
let i be non empty homogeneous quasi_total 3 -ary PartFunc of (X *),X; :: thesis:
let w be non empty homogeneous quasi_total 2 -ary PartFunc of (X *),X; :: thesis:
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

let a be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis:
assume a in rng (<*e,c*> ^ <*i,w*>) ; :: thesis:
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; :: thesis:

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 ; :: thesis:
thus the carrier of S = X ; :: thesis:
thus the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> ; :: thesis:
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 ;
A5: <*e,c*> . 2 = c ;
A6: <*i,w*> . 1 = i ;
A7: <*i,w*> . 2 = w ;
thus 1 in dom the charact of S by A3; :: according to AOFA_000:def 10 :: thesis:
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; :: thesis:
thus 2 in dom the charact of S by A3; :: according to AOFA_000:def 11 :: thesis:
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; :: thesis:
thus S is unital :: thesis:

take c ; :: according to AOFA_000:def 15 :: thesis:
thus c = the charact of S . 2 by A5, A10, FINSEQ_1:def 7; :: thesis:
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; :: thesis:

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; :: according to AOFA_000:def 14 :: thesis:
thus 3 in dom the charact of S by A3; :: according to AOFA_000:def 12 :: thesis:
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; :: thesis:
thus 4 in dom the charact of S by A3; :: according to AOFA_000:def 13 :: thesis:
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; :: thesis:
thus S is quasi_total :: thesis:

let i be Nat; :: according to UNIALG_1:def 2,MARGREL1:def 24 :: thesis:
let h be PartFunc of ( the carrier of S *), the carrier of S; :: thesis:
assume i in dom the charact of S ; :: thesis:
hence ( not h = the charact of S . i or h is quasi_total ) by A3, A11, A12, A20, A21, ENUMSET1:def 2, FINSEQ_3:2; :: thesis:

end;

let i be Nat; :: according to UNIALG_1:def 1,MARGREL1:def 23 :: thesis:
let h be PartFunc of ( the carrier of S *), the carrier of S; :: thesis:
assume that
A22: i in dom the charact of S and
A23: h = the charact of S . i ; :: thesis:
let p1, p2 be FinSequence; :: according to MARGREL1:def 1,MARGREL1:def 21 :: thesis:
( 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; :: thesis: