defpred S1[ object , object ] means for pj being Element of I *
for rj being Element of I st pj = p . $1 & rj = r . $1 holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . $1 & g = G . $1 holds
$2 = [[:f,g:]];
A1:
for j being object st j in J holds
ex i being object st S1[j,i]
proof
let j be
object ;
( j in J implies ex i being object st S1[j,i] )
assume A2:
j in J
;
ex i being object st S1[j,i]
then reconsider pj =
p . j as
Element of
I * by FUNCT_2:5;
reconsider rj =
r . j as
Element of
I by A2, FUNCT_2:5;
A3:
j in dom r
by A2, FUNCT_2:def 1;
then A4:
A . (r . j) = (A * r) . j
by FUNCT_1:13;
A5:
B . (r . j) = (B * r) . j
by A3, FUNCT_1:13;
A6:
j in dom p
by A2, FUNCT_2:def 1;
then
(A #) . (p . j) = ((A #) * p) . j
by FUNCT_1:13;
then reconsider f =
F . j as
Function of
((A #) . pj),
(A . rj) by A2, A4, PBOOLE:def 15;
(B #) . (p . j) = ((B #) * p) . j
by A6, FUNCT_1:13;
then reconsider g =
G . j as
Function of
((B #) . pj),
(B . rj) by A2, A5, PBOOLE:def 15;
take
[[:f,g:]]
;
S1[j,[[:f,g:]]]
thus
S1[
j,
[[:f,g:]]]
;
verum
end;
consider h being Function such that
A7:
( dom h = J & ( for j being object st j in J holds
S1[j,h . j] ) )
from CLASSES1:sch 1(A1);
reconsider h = h as ManySortedSet of J by A7, PARTFUN1:def 2, RELAT_1:def 18;
for j being object st j in dom h holds
h . j is Function
proof
let j be
object ;
( j in dom h implies h . j is Function )
assume A8:
j in dom h
;
h . j is Function
then reconsider pj =
p . j as
Element of
I * by A7, FUNCT_2:5;
reconsider rj =
r . j as
Element of
I by A7, A8, FUNCT_2:5;
A9:
j in dom r
by A7, A8, FUNCT_2:def 1;
then A10:
A . (r . j) = (A * r) . j
by FUNCT_1:13;
A11:
B . (r . j) = (B * r) . j
by A9, FUNCT_1:13;
A12:
j in dom p
by A7, A8, FUNCT_2:def 1;
then
(A #) . (p . j) = ((A #) * p) . j
by FUNCT_1:13;
then reconsider f =
F . j as
Function of
((A #) . pj),
(A . rj) by A7, A8, A10, PBOOLE:def 15;
(B #) . (p . j) = ((B #) * p) . j
by A12, FUNCT_1:13;
then reconsider g =
G . j as
Function of
((B #) . pj),
(B . rj) by A7, A8, A11, PBOOLE:def 15;
h . j = [[:f,g:]]
by A7, A8;
hence
h . j is
Function
;
verum
end;
then reconsider h = h as ManySortedFunction of J by FUNCOP_1:def 6;
for j being object st j in J holds
h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j)
proof
let j be
object ;
( j in J implies h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j) )
assume A13:
j in J
;
h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j)
then reconsider pj =
p . j as
Element of
I * by FUNCT_2:5;
reconsider rj =
r . j as
Element of
I by A13, FUNCT_2:5;
A14:
j in dom p
by A13, FUNCT_2:def 1;
then A15:
(([|A,B|] #) * p) . j = ([|A,B|] #) . (p . j)
by FUNCT_1:13;
A16:
j in dom r
by A13, FUNCT_2:def 1;
then A17:
A . (r . j) = (A * r) . j
by FUNCT_1:13;
A18:
([|A,B|] * r) . j = [|A,B|] . (r . j)
by A16, FUNCT_1:13;
A19:
B . (r . j) = (B * r) . j
by A16, FUNCT_1:13;
(B #) . (p . j) = ((B #) * p) . j
by A14, FUNCT_1:13;
then reconsider g =
G . j as
Function of
((B #) . pj),
(B . rj) by A13, A19, PBOOLE:def 15;
(A #) . (p . j) = ((A #) * p) . j
by A14, FUNCT_1:13;
then reconsider f =
F . j as
Function of
((A #) . pj),
(A . rj) by A13, A17, PBOOLE:def 15;
h . j = [[:f,g:]]
by A7, A13;
hence
h . j is
Function of
((([|A,B|] #) * p) . j),
(([|A,B|] * r) . j)
by A15, A18;
verum
end;
then reconsider h = h as ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r by PBOOLE:def 15;
take
h
; for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
h . j = [[:f,g:]]
thus
for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
h . j = [[:f,g:]]
by A7; verum