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

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 by FUNCT_2:113; :: thesis: verum