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 let i be Nat; :: according to MARGREL1:def 23,UNIALG_1:def 1 :: thesis: for b₁ being Element of bool [:( the carrier of S *), the carrier of S:] holds
( not i in dom the charact of S or not b₁ = the charact of S . i or b₁ 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