let A, B be non empty set ; :: thesis: for f being Function of A,B holds sproduct f = sproduct (f | { x where x is Element of A : f . x <> {} } )
let f be Function of A,B; :: thesis: sproduct f = sproduct (f | { x where x is Element of A : f . x <> {} } )
set X = { x where x is Element of A : f . x <> {} } ;
thus sproduct f c= sproduct (f | { x where x is Element of A : f . x <> {} } ) :: according to XBOOLE_0:def 10 :: thesis: sproduct (f | { x where x is Element of A : f . x <> {} } ) c= sproduct f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sproduct f or x in sproduct (f | { x where x is Element of A : f . x <> {} } ) )
assume x in sproduct f ; :: thesis: x in sproduct (f | { x where x is Element of A : f . x <> {} } )
then consider g being Function such that
A1: ( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) by Def9;

A2: now

let x be set ; :: thesis: ( x in dom g implies x in { x where x is Element of A : f . x <> {} } )
assume A3: x in dom g ; :: thesis: x in { x where x is Element of A : f . x <> {} }
then reconsider a = x as Element of A by A1, FUNCT_2:def 1;
f . a <> {} by A1, A3;
hence x in { x where x is Element of A : f . x <> {} } ; :: thesis: verum

end;

A4: now

let x be set ; :: thesis: ( x in dom g implies x in (dom f) /\ { x where x is Element of A : f . x <> {} } )
assume A5: x in dom g ; :: thesis: x in (dom f) /\ { x where x is Element of A : f . x <> {} }
then x in { x where x is Element of A : f . x <> {} } by A2;
hence x in (dom f) /\ { x where x is Element of A : f . x <> {} } by A1, A5, XBOOLE_0:def 4; :: thesis: verum

end;

A6: dom g c= dom (f | { x where x is Element of A : f . x <> {} } )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom g or x in dom (f | { x where x is Element of A : f . x <> {} } ) )
assume x in dom g ; :: thesis: x in dom (f | { x where x is Element of A : f . x <> {} } )
then x in (dom f) /\ { x where x is Element of A : f . x <> {} } by A4;
hence x in dom (f | { x where x is Element of A : f . x <> {} } ) by RELAT_1:90; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom g implies g . x in (f | { x where x is Element of A : f . x <> {} } ) . x )
assume x in dom g ; :: thesis: g . x in (f | { x where x is Element of A : f . x <> {} } ) . x
then ( x in (dom f) /\ { x where x is Element of A : f . x <> {} } & g . x in f . x ) by A1, A4;
hence g . x in (f | { x where x is Element of A : f . x <> {} } ) . x by FUNCT_1:71; :: thesis: verum

end;

hence x in sproduct (f | { x where x is Element of A : f . x <> {} } ) by A1, A6, Def9; :: thesis: verum

end;

thus sproduct (f | { x where x is Element of A : f . x <> {} } ) c= sproduct f by Th72, RELAT_1:88; :: thesis: verum