theorem Th02: :: ABSRED_0:160

for X being non empty set
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 )