A1:
dom A = I
by PARTFUN1:def 2;

dom B = J by PARTFUN1:def 2;

hence ( A cc= B implies ( I c= J & ( for i being set st i in I holds

A . i c= B . i ) ) ) by A1; :: thesis: ( I c= J & ( for i being set st i in I holds

A . i c= B . i ) implies A cc= B )

assume that

A2: I c= J and

A3: for i being set st i in I holds

A . i c= B . i ; :: thesis: A cc= B

thus dom A c= dom B by A1, A2, PARTFUN1:def 2; :: according to ALTCAT_2:def 1 :: thesis: for i being set st i in dom A holds

A . i c= B . i

let i be set ; :: thesis: ( i in dom A implies A . i c= B . i )

assume i in dom A ; :: thesis: A . i c= B . i

hence A . i c= B . i by A1, A3; :: thesis: verum

dom B = J by PARTFUN1:def 2;

hence ( A cc= B implies ( I c= J & ( for i being set st i in I holds

A . i c= B . i ) ) ) by A1; :: thesis: ( I c= J & ( for i being set st i in I holds

A . i c= B . i ) implies A cc= B )

assume that

A2: I c= J and

A3: for i being set st i in I holds

A . i c= B . i ; :: thesis: A cc= B

thus dom A c= dom B by A1, A2, PARTFUN1:def 2; :: according to ALTCAT_2:def 1 :: thesis: for i being set st i in dom A holds

A . i c= B . i

let i be set ; :: thesis: ( i in dom A implies A . i c= B . i )

assume i in dom A ; :: thesis: A . i c= B . i

hence A . i c= B . i by A1, A3; :: thesis: verum