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 object ; :: 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 and
A2: dom g c= dom f and
A3: for x being object st x in dom g holds
g . x in f . x by Def9;

A4: now :: thesis: for x being object st x in dom g holds
x in { x where x is Element of A : f . x <> {} }

let x be object ; :: thesis: ( x in dom g implies x in { x where x is Element of A : f . x <> {} } )
assume A5: 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 A2, FUNCT_2:def 1;
f . a <> {} by A3, A5;
hence x in { x where x is Element of A : f . x <> {} } ; :: thesis: verum

end;

A6: now :: thesis: for x being object st x in dom g holds
x in (dom f) /\ { x where x is Element of A : f . x <> {} }

let x be object ; :: thesis: ( x in dom g implies x in (dom f) /\ { x where x is Element of A : f . x <> {} } )
assume A7: 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 A4;
hence x in (dom f) /\ { x where x is Element of A : f . x <> {} } by A2, A7, XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

let x be object ; :: 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 A6;
hence x in dom (f | { x where x is Element of A : f . x <> {} } ) by RELAT_1:61; :: thesis: verum

end;

now :: thesis: for x being object st x in dom g holds
g . x in (f | { x where x is Element of A : f . x <> {} } ) . x

let x be object ; :: thesis: ( x in dom g implies g . x in (f | { x where x is Element of A : f . x <> {} } ) . x )
assume A9: x in dom g ; :: thesis: g . x in (f | { x where x is Element of A : f . x <> {} } ) . x
then g . x in f . x by A3;
hence g . x in (f | { x where x is Element of A : f . x <> {} } ) . x by A6, A9, FUNCT_1:48; :: thesis: verum

end;

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

end;

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