let IT1, IT2 be non empty strict Language-like ; ( the adicity of IT1 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of IT1 = the ZeroF of L & the OneF of IT1 = the OneF of L & the adicity of IT2 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of IT2 = the ZeroF of L & the OneF of IT2 = the OneF of L implies IT1 = IT2 )
set c1 = the carrier of IT1;
set z1 = the ZeroF of IT1;
set o1 = the OneF of IT1;
set a1 = the adicity of IT1;
set c2 = the carrier of IT2;
set z2 = the ZeroF of IT2;
set o2 = the OneF of IT2;
set a2 = the adicity of IT2;
set ITT1 = Language-like(# the carrier of IT1, the ZeroF of IT1, the OneF of IT1, the adicity of IT1 #);
set ITT2 = Language-like(# the carrier of IT2, the ZeroF of IT2, the OneF of IT2, the adicity of IT2 #);
reconsider ITT1 = Language-like(# the carrier of IT1, the ZeroF of IT1, the OneF of IT1, the adicity of IT1 #), ITT2 = Language-like(# the carrier of IT2, the ZeroF of IT2, the OneF of IT2, the adicity of IT2 #) as non empty Language-like ;
defpred S1[ Language-like ] means ( the adicity of $1 = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of $1 = the ZeroF of L & the OneF of $1 = the OneF of L );
assume A2:
( S1[IT1] & S1[IT2] )
; IT1 = IT2
dom the adicity of IT1 = the carrier of IT2 \ { the OneF of IT1}
by FUNCT_2:def 1, A2;
then ( the carrier of IT1 \ { the OneF of IT1}) \/ ({ the OneF of IT1} null the carrier of IT1) =
( the carrier of IT2 \ { the OneF of IT2}) \/ ({ the OneF of IT2} null the carrier of IT2)
by A2, FUNCT_2:def 1
.=
the carrier of IT2
;
hence
IT1 = IT2
by A2; verum