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
A8: for s being OperSymbol of (CatSign the carrier of C1) holds U1 . s = [(s `1 ),((Obj F) * (s `2 ))] and
A9: for s being OperSymbol of (CatSign the carrier of C1) holds U2 . s = [(s `1 ),((Obj F) * (s `2 ))] ; :: thesis: U1 = U2

now

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 A8
.= U2 . s by A9 ; :: thesis: verum

end;

hence U1 = U2 by FUNCT_2:113; :: thesis: verum