let A be partial non-empty UAStr ; :: thesis:
set P = SmallestPartition the carrier of A;
let f be operation of A; :: thesis:

hereby :: according to PUA2MSS1:def 8,PUA2MSS1:def 9 :: thesis:

let p be FinSequence of SmallestPartition the carrier of A; :: thesis:
consider q being FinSequence of the carrier of A such that
A1: product p = {q} by Th12;
( ( q in dom f & f . q in rng f & rng f c= the carrier of A ) or not q in dom f ) by FUNCT_1:def 3;
then consider x being Element of A such that
A2: ( ( q in dom f & x = f . q ) or not q in dom f ) ;
SmallestPartition the carrier of A = { {z} where z is Element of A : verum } by EQREL_1:37;
then {x} in SmallestPartition the carrier of A ;
then reconsider a = {x} as Element of SmallestPartition the carrier of A ;
take a = a; :: thesis:
thus f .: (product p) c= a :: thesis:

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in f .: (product p) ; :: thesis:
then consider y being object such that
A3: y in dom f and
A4: y in product p and
A5: z = f . y by FUNCT_1:def 6;
y = q by A1, A4, TARSKI:def 1;
hence z in a by A2, A3, A5, TARSKI:def 1; :: thesis:

end;

end;

let p be FinSequence of SmallestPartition the carrier of A; :: thesis:
consider q being FinSequence of the carrier of A such that
A6: product p = {q} by Th12;
assume product p meets dom f ; :: thesis:
then A7: ex x being object st
( x in product p & x in dom f ) by XBOOLE_0:3;
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in product p ; :: thesis:
then z = q by A6, TARSKI:def 1;
hence z in dom f by A6, A7, TARSKI:def 1; :: thesis: