let E1, E2 be strict Category; :: thesis:
assume that
A55: the carrier of E1 = commaObjs F,G and
A56: the carrier' of E1 = commaMorphs F,G and
A57: for k being Element of commaMorphs F,G holds the Source of E1 . k = k `11 and
A58: for k being Element of commaMorphs F,G holds the Target of E1 . k = k `12 and
A59: for o being Element of commaObjs F,G holds the Id of E1 . o = [[o,o],[(id (o `11 )),(id (o `12 ))]] and
A60: the Comp of E1 = commaComp F,G and
A61: ( the carrier of E2 = commaObjs F,G & the carrier' of E2 = commaMorphs F,G ) and
A62: for k being Element of commaMorphs F,G holds the Source of E2 . k = k `11 and
A63: for k being Element of commaMorphs F,G holds the Target of E2 . k = k `12 and
A64: for o being Element of commaObjs F,G holds the Id of E2 . o = [[o,o],[(id (o `11 )),(id (o `12 ))]] and
A65: the Comp of E2 = commaComp F,G ; :: thesis:

now

let x be Element of H₂(E1); :: thesis:
thus the Target of E1 . x = x `12 by A56, A58
.= the Target of E2 . x by A56, A63 ; :: thesis:

end;

then A66: the Target of E1 = the Target of E2 by A55, A56, A61, FUNCT_2:113;

A67: now

let x be Object of E1; :: thesis:
reconsider o = x as Element of commaObjs F,G by A55;
thus the Id of E1 . x = [[o,o],[(id (o `11 )),(id (o `12 ))]] by A59
.= the Id of E2 . x by A64 ; :: thesis:

end;

now

let x be Element of H₂(E1); :: thesis:
thus the Source of E1 . x = x `11 by A56, A57
.= the Source of E2 . x by A56, A62 ; :: thesis:

end;

then the Source of E1 = the Source of E2 by A55, A56, A61, FUNCT_2:113;
hence E1 = E2 by A55, A56, A60, A61, A65, A66, A67, FUNCT_2:113; :: thesis: