defpred S1[ Element of product a, Element of product a, Element of product a] means for i being Element of dom a holds $3 . i = (b . i) . (($1 . i),($2 . i));
A1:
for f, g being Element of product a ex z being Element of product a st S1[f,g,z]
proof
let f,
g be
Element of
product a;
ex z being Element of product a st S1[f,g,z]
defpred S2[
object ,
object ]
means ex
i being
Element of
dom a st
( $1
= i & $2
= (b . i) . (
(f . i),
(g . i)) );
A2:
for
x being
object st
x in dom a holds
ex
z being
object st
S2[
x,
z]
proof
let x be
object ;
( x in dom a implies ex z being object st S2[x,z] )
assume
x in dom a
;
ex z being object st S2[x,z]
then reconsider i =
x as
Element of
dom a ;
take
(b . i) . (
(f . i),
(g . i))
;
S2[x,(b . i) . ((f . i),(g . i))]
thus
S2[
x,
(b . i) . (
(f . i),
(g . i))]
;
verum
end;
consider z being
Function such that A3:
(
dom z = dom a & ( for
x being
object st
x in dom a holds
S2[
x,
z . x] ) )
from CLASSES1:sch 1(A2);
then reconsider z9 =
z as
Element of
product a by A3, CARD_3:9;
take
z9
;
S1[f,g,z9]
let i be
Element of
dom a;
z9 . i = (b . i) . ((f . i),(g . i))
ex
j being
Element of
dom a st
(
j = i &
z . i = (b . j) . (
(f . j),
(g . j)) )
by A3;
hence
z9 . i = (b . i) . (
(f . i),
(g . i))
;
verum
end;
consider d being BinOp of (product a) such that
A4:
for f, g being Element of product a holds S1[f,g,d . (f,g)]
from BINOP_1:sch 3(A1);
take
d
; for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i))
thus
for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i))
by A4; verum