let f1, f2 be Function of the adjectives of T, the carrier of T; :: thesis: ( ( for a being adjective of T holds f1 . a = sup ((types a) \/ (types (non- a))) ) & ( for a being adjective of T holds f2 . a = sup ((types a) \/ (types (non- a))) ) implies f1 = f2 )
assume that
A2: for a being adjective of T holds f1 . a = sup ((types a) \/ (types (non- a))) and
A3: for a being adjective of T holds f2 . a = sup ((types a) \/ (types (non- a))) ; :: thesis: f1 = f2

now :: thesis: for a being Element of the adjectives of T holds f1 . a = f2 . a

let a be Element of the adjectives of T; :: thesis: f1 . a = f2 . a
reconsider b = a as adjective of T ;
thus f1 . a = sup ((types b) \/ (types (non- b))) by A2
.= f2 . a by A3 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum