let U1, U2 be Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2); :: thesis: ( ( for s being SortSymbol of (CatSign the carrier of C1) holds U1 . s = [0,((Obj F) * (s `2))] ) & ( for s being SortSymbol of (CatSign the carrier of C1) holds U2 . s = [0,((Obj F) * (s `2))] ) implies U1 = U2 )
assume that
A1: for s being SortSymbol of (CatSign the carrier of C1) holds U1 . s = [0,((Obj F) * (s `2))] and
A2: for s being SortSymbol of (CatSign the carrier of C1) holds U2 . s = [0,((Obj F) * (s `2))] ; :: thesis: U1 = U2

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

let s be SortSymbol of (CatSign the carrier of C1); :: thesis: U1 . s = U2 . s
thus U1 . s = [0,((Obj F) * (s `2))] by A1
.= U2 . s by A2 ; :: thesis: verum

end;

hence U1 = U2 ; :: thesis: verum