let IT1, IT2 be non empty strict Language-like ; :: thesis: ( 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 S₁[ 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: ( S₁[IT1] & S₁[IT2] ) ; :: thesis: 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; :: thesis: verum