let E1, E2 be strict Category; :: thesis: ( the carrier of E1 = commaObjs (F,G) & the carrier' of E1 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of E1 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of E1 . k = k `12 ) & ( for o being Element of commaObjs (F,G) holds the Id of E1 . o = [[o,o],[(id (o `11)),(id (o `12))]] ) & the Comp of E1 = commaComp (F,G) & the carrier of E2 = commaObjs (F,G) & the carrier' of E2 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of E2 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of E2 . k = k `12 ) & ( for o being Element of commaObjs (F,G) holds the Id of E2 . o = [[o,o],[(id (o `11)),(id (o `12))]] ) & the Comp of E2 = commaComp (F,G) implies E1 = E2 )
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: E1 = E2

now

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

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: the Id of E1 . x = the Id of E2 . x
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: verum

end;

now

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

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: verum