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 ) & 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 ) & the Comp of E2 = commaComp (F,G) implies E1 = E2 )
assume that
A104: the carrier of E1 = commaObjs (F,G) and
A105: the carrier' of E1 = commaMorphs (F,G) and
A106: for k being Element of commaMorphs (F,G) holds the Source of E1 . k = k `11 and
A107: for k being Element of commaMorphs (F,G) holds the Target of E1 . k = k `12 and
A108: the Comp of E1 = commaComp (F,G) and
A109: ( the carrier of E2 = commaObjs (F,G) & the carrier' of E2 = commaMorphs (F,G) ) and
A110: for k being Element of commaMorphs (F,G) holds the Source of E2 . k = k `11 and
A111: for k being Element of commaMorphs (F,G) holds the Target of E2 . k = k `12 and
A112: the Comp of E2 = commaComp (F,G) ; :: thesis: E1 = E2

now :: thesis: for x being Element of H₂(E1) holds the Target of E1 . x = the Target of E2 . x

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 A105, A107
.= the Target of E2 . x by A105, A111 ; :: thesis: verum

end;

then A113: the Target of E1 = the Target of E2 by A104, A105, A109, FUNCT_2:63;

now :: thesis: for x being Element of H₂(E1) holds the Source of E1 . x = the Source of E2 . x

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 A105, A106
.= the Source of E2 . x by A105, A110 ; :: thesis: verum

end;

then the Source of E1 = the Source of E2 by A104, A105, A109, FUNCT_2:63;
hence E1 = E2 by A104, A105, A108, A109, A112, A113; :: thesis: verum