let X be non empty set ; :: thesis: for f1, f2, f3 being non empty homogeneous quasi_total PartFunc of (X *),X

for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> = the charact of S holds

( S is quasi_total & S is partial )

let f1, f2, f3 be non empty homogeneous quasi_total PartFunc of (X *),X; :: thesis: for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> = the charact of S holds

( S is quasi_total & S is partial )

let S be non empty UAStr ; :: thesis: ( the carrier of S = X & <*f1,f2,f3*> = the charact of S implies ( S is quasi_total & S is partial ) )

assume 04: ( the carrier of S = X & <*f1,f2,f3*> = the charact of S ) ; :: thesis: ( S is quasi_total & S is partial )

set A = the carrier of S;

thus S is quasi_total :: thesis: S is partial_{1} being Element of bool [:( the carrier of S *), the carrier of S:] holds

( not i in dom the charact of S or not b_{1} = the charact of S . i or b_{1} is homogeneous )

let h be PartFunc of ( the carrier of S *), the carrier of S; :: thesis: ( not i in dom the charact of S or not h = the charact of S . i or h is homogeneous )

assume i in dom the charact of S ; :: thesis: ( not h = the charact of S . i or h is homogeneous )

then i in Seg 3 by 04, FINSEQ_1:89;

then ( i = 1 or i = 2 or i = 3 ) by FINSEQ_3:1, ENUMSET1:def 1;

hence ( not h = the charact of S . i or h is homogeneous ) by 04, FINSEQ_1:45; :: thesis: verum

for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> = the charact of S holds

( S is quasi_total & S is partial )

let f1, f2, f3 be non empty homogeneous quasi_total PartFunc of (X *),X; :: thesis: for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> = the charact of S holds

( S is quasi_total & S is partial )

let S be non empty UAStr ; :: thesis: ( the carrier of S = X & <*f1,f2,f3*> = the charact of S implies ( S is quasi_total & S is partial ) )

assume 04: ( the carrier of S = X & <*f1,f2,f3*> = the charact of S ) ; :: thesis: ( S is quasi_total & S is partial )

set A = the carrier of S;

thus S is quasi_total :: thesis: S is partial

proof

let i be Nat; :: according to MARGREL1:def 23,UNIALG_1:def 1 :: thesis: for b
let i be Nat; :: according to MARGREL1:def 24,UNIALG_1:def 2 :: thesis: for b_{1} being Element of bool [:( the carrier of S *), the carrier of S:] holds

( not i in dom the charact of S or not b_{1} = the charact of S . i or b_{1} is quasi_total )

let h be PartFunc of ( the carrier of S *), the carrier of S; :: thesis: ( not i in dom the charact of S or not h = the charact of S . i or h is quasi_total )

assume i in dom the charact of S ; :: thesis: ( not h = the charact of S . i or h is quasi_total )

then i in Seg 3 by 04, FINSEQ_1:89;

then ( i = 1 or i = 2 or i = 3 ) by FINSEQ_3:1, ENUMSET1:def 1;

hence ( not h = the charact of S . i or h is quasi_total ) by 04, FINSEQ_1:45; :: thesis: verum

end;( not i in dom the charact of S or not b

let h be PartFunc of ( the carrier of S *), the carrier of S; :: thesis: ( not i in dom the charact of S or not h = the charact of S . i or h is quasi_total )

assume i in dom the charact of S ; :: thesis: ( not h = the charact of S . i or h is quasi_total )

then i in Seg 3 by 04, FINSEQ_1:89;

then ( i = 1 or i = 2 or i = 3 ) by FINSEQ_3:1, ENUMSET1:def 1;

hence ( not h = the charact of S . i or h is quasi_total ) by 04, FINSEQ_1:45; :: thesis: verum

( not i in dom the charact of S or not b

let h be PartFunc of ( the carrier of S *), the carrier of S; :: thesis: ( not i in dom the charact of S or not h = the charact of S . i or h is homogeneous )

assume i in dom the charact of S ; :: thesis: ( not h = the charact of S . i or h is homogeneous )

then i in Seg 3 by 04, FINSEQ_1:89;

then ( i = 1 or i = 2 or i = 3 ) by FINSEQ_3:1, ENUMSET1:def 1;

hence ( not h = the charact of S . i or h is homogeneous ) by 04, FINSEQ_1:45; :: thesis: verum