let U1, U2 be Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2); :: thesis: ( ( for o being OperSymbol of (CatSign the carrier of C1) holds U1 . o = [(o `1),((Obj F) * (o `2))] ) & ( for o being OperSymbol of (CatSign the carrier of C1) holds U2 . o = [(o `1),((Obj F) * (o `2))] ) implies U1 = U2 )
assume that
A13: for s being OperSymbol of (CatSign the carrier of C1) holds U1 . s = [(s `1),((Obj F) * (s `2))] and
A14: for s being OperSymbol of (CatSign the carrier of C1) holds U2 . s = [(s `1),((Obj F) * (s `2))] ; :: thesis: U1 = U2

now :: thesis: for s being OperSymbol of (CatSign the carrier of C1) holds U1 . s = U2 . s

let s be OperSymbol of (CatSign the carrier of C1); :: thesis: U1 . s = U2 . s
thus U1 . s = [(s `1),((Obj F) * (s `2))] by A13
.= U2 . s by A14 ; :: thesis: verum

end;

hence U1 = U2 ; :: thesis: verum