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