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

hereby :: according to PUA2MSS1:def 8,PUA2MSS1:def 9 :: thesis: for p being FinSequence of SmallestPartition the carrier of A st product p meets dom f holds
product p c= dom f

let p be FinSequence of SmallestPartition the carrier of A; :: thesis: ex a being Element of SmallestPartition the carrier of A st f .: (product p) c= a
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: f .: (product p) c= a
thus f .: (product p) c= a :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f .: (product p) or z in a )
assume z in f .: (product p) ; :: thesis: z in a
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: verum

end;

end;

let p be FinSequence of SmallestPartition the carrier of A; :: thesis: ( product p meets dom f implies product p c= dom f )
consider q being FinSequence of the carrier of A such that
A6: product p = {q} by Th12;
assume product p meets dom f ; :: thesis: product p c= dom f
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: ( not z in product p or z in dom f )
assume z in product p ; :: thesis: z in dom f
then z = q by A6, TARSKI:def 1;
hence z in dom f by A6, A7, TARSKI:def 1; :: thesis: verum