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

end;

then A115: the Target of E1 = the Target of E2 by A106, A107, A111, 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 A107, A108
.= the Source of E2 . x by A107, A112 ; :: thesis: verum

end;

then the Source of E1 = the Source of E2 by A106, A107, A111, FUNCT_2:63;
hence E1 = E2 by A106, A107, A110, A111, A114, A115; :: thesis: verum