let A be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( o1 c= o2 implies o1,D .: A c= o2,E .: A )
assume A1:
o1 c= o2
; :: thesis: o1,D .: A c= o2,E .: A
then A2:
( dom o1 c= dom o2 & dom o1 = [:D1,D2:] & dom o2 = [:E1,E2:] & dom (o1,D .: A) = [:(Funcs A,D1),(Funcs A,D2):] & dom (o2,E .: A) = [:(Funcs A,E1),(Funcs A,E2):] & ( for x being set st x in dom o1 holds
o1 . x = o2 . x ) )
by FUNCT_2:def 1, GRFUNC_1:8;
then
( D1 c= E1 & D2 c= E2 )
by ZFMISC_1:138;
then A3:
( Funcs A,D1 c= Funcs A,E1 & Funcs A,D2 c= Funcs A,E2 )
by FUNCT_5:63;
then A4:
dom (o1,D .: A) c= dom (o2,E .: A)
by A2, ZFMISC_1:119;
now let x be
set ;
:: thesis: ( x in dom (o1,D .: A) implies (o1,D .: A) . x = (o2,E .: A) . x )assume
x in dom (o1,D .: A)
;
:: thesis: (o1,D .: A) . x = (o2,E .: A) . xthen reconsider y =
x as
Element of
[:(Funcs A,D1),(Funcs A,D2):] ;
reconsider f1 =
y `1 as
Element of
Funcs A,
D1 ;
reconsider g1 =
y `1 as
Element of
Funcs A,
E1 by A3, TARSKI:def 3;
reconsider f2 =
y `2 as
Element of
Funcs A,
D2 ;
reconsider g2 =
y `2 as
Element of
Funcs A,
E2 by A3, TARSKI:def 3;
A5:
(
(o1,D .: A) . f1,
f2 = o1 .: f1,
f2 &
(o2,E .: A) . g1,
g2 = o2 .: g1,
g2 &
rng f1 c= D1 &
rng f2 c= D2 &
dom f1 = A &
dom f2 = A &
dom (o2 .: g1,g2) = A &
dom (o1 .: f1,f2) = A )
by Def2, FUNCT_2:def 1;
now let z be
set ;
:: thesis: ( z in A implies (o2 .: g1,g2) . z = (o1 .: f1,f2) . z )assume
z in A
;
:: thesis: (o2 .: g1,g2) . z = (o1 .: f1,f2) . zthen A6:
(
(o2 .: g1,g2) . z = o2 . (g1 . z),
(g2 . z) &
(o1 .: f1,f2) . z = o1 . (f1 . z),
(f2 . z) &
o1 . (f1 . z),
(f2 . z) = o1 . [(f1 . z),(f2 . z)] &
o2 . (f1 . z),
(f2 . z) = o2 . [(f1 . z),(f2 . z)] &
f1 . z in rng f1 &
f2 . z in rng f2 )
by A5, FUNCOP_1:28, FUNCT_1:def 5;
then
[(f1 . z),(f2 . z)] in dom o1
by A2, ZFMISC_1:106;
hence
(o2 .: g1,g2) . z = (o1 .: f1,f2) . z
by A1, A6, GRFUNC_1:8;
:: thesis: verum end; then
(
(o1,D .: A) . f1,
f2 = (o1,D .: A) . [f1,f2] &
[f1,f2] = x &
(o2,E .: A) . g1,
g2 = (o2,E .: A) . [g1,g2] &
o2 .: g1,
g2 = o1 .: f1,
f2 )
by A5, FUNCT_1:9, MCART_1:23;
hence
(o1,D .: A) . x = (o2,E .: A) . x
by A5;
:: thesis: verum end;
hence
o1,D .: A c= o2,E .: A
by A4, GRFUNC_1:8; :: thesis: verum