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 )
A1: dom o1 = [:D1,D2:] by FUNCT_2:def 1;
assume A2: o1 c= o2 ; :: thesis: o1,D .: A c= o2,E .: A
then A3: dom o1 c= dom o2 by GRFUNC_1:8;
A4: dom o2 = [:E1,E2:] by FUNCT_2:def 1;
then D2 c= E2 by A3, A1, ZFMISC_1:138;
then A5: Funcs A,D2 c= Funcs A,E2 by FUNCT_5:63;
D1 c= E1 by A3, A1, A4, ZFMISC_1:138;
then A6: Funcs A,D1 c= Funcs A,E1 by FUNCT_5:63;

A7: 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) . x
then reconsider y = x as Element of [:(Funcs A,D1),(Funcs A,D2):] ;
reconsider g2 = y `2 as Element of Funcs A,E2 by A5, TARSKI:def 3;
reconsider f2 = y `2 as Element of Funcs A,D2 ;
reconsider g1 = y `1 as Element of Funcs A,E1 by A6, TARSKI:def 3;
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

let z be set ; :: thesis: ( z in A implies (o2 .: g1,g2) . z = (o1 .: f1,f2) . z )
assume A11: z in A ; :: thesis: (o2 .: g1,g2) . z = (o1 .: f1,f2) . z
then ( f1 . z in rng f1 & f2 . z in rng f2 ) by A9, FUNCT_1:def 5;
then A12: [(f1 . z),(f2 . z)] in dom o1 by A1, ZFMISC_1:106;
( (o2 .: g1,g2) . z = o2 . (g1 . z),(g2 . z) & (o1 .: f1,f2) . z = o1 . (f1 . z),(f2 . z) ) by A8, A11, FUNCOP_1:28;
hence (o2 .: g1,g2) . z = (o1 .: f1,f2) . z by A2, A12, GRFUNC_1:8; :: thesis: verum

end;

A13: [f1,f2] = x by MCART_1:23;
( (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:9; :: thesis: 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:119;
hence o1,D .: A c= o2,E .: A by A7, GRFUNC_1:8; :: thesis: verum