let I be set ; :: thesis: for f, g being ManySortedSet of I holds (product f) /\ (product g) = product (f (/\) g)

let f, g be ManySortedSet of I; :: thesis: (product f) /\ (product g) = product (f (/\) g)

for x being object holds

( x in (product f) /\ (product g) iff ex h being Function st

( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) ) )

let f, g be ManySortedSet of I; :: thesis: (product f) /\ (product g) = product (f (/\) g)

for x being object holds

( x in (product f) /\ (product g) iff ex h being Function st

( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) ) )

proof

hence
(product f) /\ (product g) = product (f (/\) g)
by CARD_3:def 5; :: thesis: verum
let x be object ; :: thesis: ( x in (product f) /\ (product g) iff ex h being Function st

( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) ) )

A8: for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ; :: thesis: x in (product f) /\ (product g)

a9: dom h = I by A7, PARTFUN1:def 2;

then A9: ( dom h = dom f & dom h = dom g ) by PARTFUN1:def 2;

h . y in f . y by A10;

then A13: h in product f by A9, CARD_3:9;

for y being object st y in dom g holds

h . y in g . y by A10;

then h in product g by A9, CARD_3:9;

hence x in (product f) /\ (product g) by A7, A13, XBOOLE_0:def 4; :: thesis: verum

end;( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) ) )

hereby :: thesis: ( ex h being Function st

( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) ) implies x in (product f) /\ (product g) )

given h being Function such that A7:
( h = x & dom h = dom (f (/\) g) )
and ( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) ) implies x in (product f) /\ (product g) )

assume
x in (product f) /\ (product g)
; :: thesis: ex h being Function st

( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) )

then A1: ( x in product f & x in product g ) by XBOOLE_0:def 4;

then consider h being Function such that

A2: ( h = x & dom h = dom f ) and

A3: for y being object st y in dom f holds

h . y in f . y by CARD_3:def 5;

take h = h; :: thesis: ( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) )

thus h = x by A2; :: thesis: ( dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) )

thus dom h = I by A2, PARTFUN1:def 2

.= dom (f (/\) g) by PARTFUN1:def 2 ; :: thesis: for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y

let y be object ; :: thesis: ( y in dom (f (/\) g) implies h . y in (f (/\) g) . y )

assume a4: y in dom (f (/\) g) ; :: thesis: h . y in (f (/\) g) . y

then A4: y in I ;

A5: ( y in dom f & y in dom g ) by A4, PARTFUN1:def 2;

then A6: h . y in f . y by A3;

h . y in g . y by A1, A2, A5, CARD_3:9;

then h . y in (f . y) /\ (g . y) by A6, XBOOLE_0:def 4;

hence h . y in (f (/\) g) . y by a4, PBOOLE:def 5; :: thesis: verum

end;( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) )

then A1: ( x in product f & x in product g ) by XBOOLE_0:def 4;

then consider h being Function such that

A2: ( h = x & dom h = dom f ) and

A3: for y being object st y in dom f holds

h . y in f . y by CARD_3:def 5;

take h = h; :: thesis: ( h = x & dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) )

thus h = x by A2; :: thesis: ( dom h = dom (f (/\) g) & ( for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ) )

thus dom h = I by A2, PARTFUN1:def 2

.= dom (f (/\) g) by PARTFUN1:def 2 ; :: thesis: for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y

let y be object ; :: thesis: ( y in dom (f (/\) g) implies h . y in (f (/\) g) . y )

assume a4: y in dom (f (/\) g) ; :: thesis: h . y in (f (/\) g) . y

then A4: y in I ;

A5: ( y in dom f & y in dom g ) by A4, PARTFUN1:def 2;

then A6: h . y in f . y by A3;

h . y in g . y by A1, A2, A5, CARD_3:9;

then h . y in (f . y) /\ (g . y) by A6, XBOOLE_0:def 4;

hence h . y in (f (/\) g) . y by a4, PBOOLE:def 5; :: thesis: verum

A8: for y being object st y in dom (f (/\) g) holds

h . y in (f (/\) g) . y ; :: thesis: x in (product f) /\ (product g)

a9: dom h = I by A7, PARTFUN1:def 2;

then A9: ( dom h = dom f & dom h = dom g ) by PARTFUN1:def 2;

A10: now :: thesis: for y being object st ( y in dom f or y in dom g ) holds

( h . y in f . y & h . y in g . y )

for y being object st y in dom f holds ( h . y in f . y & h . y in g . y )

let y be object ; :: thesis: ( ( y in dom f or y in dom g ) implies ( h . y in f . y & h . y in g . y ) )

assume A11: ( y in dom f or y in dom g ) ; :: thesis: ( h . y in f . y & h . y in g . y )

h . y in (f (/\) g) . y by A7, A8, a9, A11;

then h . y in (f . y) /\ (g . y) by A11, PBOOLE:def 5;

hence ( h . y in f . y & h . y in g . y ) by XBOOLE_0:def 4; :: thesis: verum

end;assume A11: ( y in dom f or y in dom g ) ; :: thesis: ( h . y in f . y & h . y in g . y )

h . y in (f (/\) g) . y by A7, A8, a9, A11;

then h . y in (f . y) /\ (g . y) by A11, PBOOLE:def 5;

hence ( h . y in f . y & h . y in g . y ) by XBOOLE_0:def 4; :: thesis: verum

h . y in f . y by A10;

then A13: h in product f by A9, CARD_3:9;

for y being object st y in dom g holds

h . y in g . y by A10;

then h in product g by A9, CARD_3:9;

hence x in (product f) /\ (product g) by A7, A13, XBOOLE_0:def 4; :: thesis: verum