let A be set ; for D1, D2, D, E1, E2, E being non empty set
for o1 being Function of [:D1,D2:],D
for o2 being Function of [:E1,E2:],E st o1 c= o2 holds
(o1,D) .: A c= (o2,E) .: A
let D1, D2, D, E1, E2, E be non empty set ; for o1 being Function of [:D1,D2:],D
for o2 being Function of [:E1,E2:],E st o1 c= o2 holds
(o1,D) .: A c= (o2,E) .: A
let o1 be Function of [:D1,D2:],D; for o2 being Function of [:E1,E2:],E st o1 c= o2 holds
(o1,D) .: A c= (o2,E) .: A
let o2 be Function of [:E1,E2:],E; ( o1 c= o2 implies (o1,D) .: A c= (o2,E) .: A )
A1:
dom o1 = [:D1,D2:]
by FUNCT_2:def 1;
assume A2:
o1 c= o2
; (o1,D) .: A c= (o2,E) .: A
then A3:
dom o1 c= dom o2
by GRFUNC_1:2;
A4:
dom o2 = [:E1,E2:]
by FUNCT_2:def 1;
then
D2 c= E2
by A3, A1, ZFMISC_1:114;
then A5:
Funcs (A,D2) c= Funcs (A,E2)
by FUNCT_5:56;
D1 c= E1
by A3, A1, A4, ZFMISC_1:114;
then A6:
Funcs (A,D1) c= Funcs (A,E1)
by FUNCT_5:56;
A7:
now for x being object st x in dom ((o1,D) .: A) holds
((o1,D) .: A) . x = ((o2,E) .: A) . xlet x be
object ;
( x in dom ((o1,D) .: A) implies ((o1,D) .: A) . x = ((o2,E) .: A) . x )assume
x in dom ((o1,D) .: A)
;
((o1,D) .: A) . x = ((o2,E) .: A) . xthen reconsider y =
x as
Element of
[:(Funcs (A,D1)),(Funcs (A,D2)):] ;
reconsider g2 =
y `2 as
Element of
Funcs (
A,
E2)
by A5;
reconsider f2 =
y `2 as
Element of
Funcs (
A,
D2) ;
reconsider g1 =
y `1 as
Element of
Funcs (
A,
E1)
by A6;
reconsider f1 =
y `1 as
Element of
Funcs (
A,
D1) ;
A8:
(
dom (o2 .: (g1,g2)) = A &
dom (o1 .: (f1,f2)) = A )
by FUNCT_2:def 1;
A9:
(
dom f1 = A &
dom f2 = A )
by FUNCT_2:def 1;
A10:
now for z being object st z in A holds
(o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . zlet z be
object ;
( z in A implies (o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . z )assume A11:
z in A
;
(o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . zthen
(
f1 . z in rng f1 &
f2 . z in rng f2 )
by A9, FUNCT_1:def 3;
then A12:
[(f1 . z),(f2 . z)] in dom o1
by A1, ZFMISC_1:87;
(
(o2 .: (g1,g2)) . z = o2 . (
(g1 . z),
(g2 . z)) &
(o1 .: (f1,f2)) . z = o1 . (
(f1 . z),
(f2 . z)) )
by A8, A11, FUNCOP_1:22;
hence
(o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . z
by A2, A12, GRFUNC_1:2;
verum end; A13:
[f1,f2] = x
by MCART_1:21;
(
((o1,D) .: A) . (
f1,
f2)
= o1 .: (
f1,
f2) &
((o2,E) .: A) . (
g1,
g2)
= o2 .: (
g1,
g2) )
by Def2;
hence
((o1,D) .: A) . x = ((o2,E) .: A) . x
by A8, A10, A13, FUNCT_1:2;
verum end;
( dom ((o1,D) .: A) = [:(Funcs (A,D1)),(Funcs (A,D2)):] & dom ((o2,E) .: A) = [:(Funcs (A,E1)),(Funcs (A,E2)):] )
by FUNCT_2:def 1;
then
dom ((o1,D) .: A) c= dom ((o2,E) .: A)
by A6, A5, ZFMISC_1:96;
hence
(o1,D) .: A c= (o2,E) .: A
by A7, GRFUNC_1:2; verum