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
proof
let i be Nat; :: according to MARGREL1:def 24,UNIALG_1:def 2 :: thesis: 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 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 ;
then ( i = 1 or i = 2 or i = 3 ) by ;
hence ( not h = the charact of S . i or h is quasi_total ) by ; :: thesis: verum
end;
let i be Nat; :: according to MARGREL1:def 23,UNIALG_1:def 1 :: thesis: 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; :: 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 ;
then ( i = 1 or i = 2 or i = 3 ) by ;
hence ( not h = the charact of S . i or h is homogeneous ) by ; :: thesis: verum