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: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 :: thesis: for x being object st x in dom ((o1,D) .: A) holds
((o1,D) .: A) . x = ((o2,E) .: A) . x

let x be object ; :: 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;
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 :: thesis: for z being object st z in A holds
(o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . z

let z be object ; :: 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 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; :: thesis: 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; :: 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:96;
hence (o1,D) .: A c= (o2,E) .: A by A7, GRFUNC_1:2; :: thesis: verum