let n be Nat; :: thesis: for s being set

for S1, S2 being non empty BoolSignature st n >= 1 & the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= n + 6 & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & ( for i being Nat st i >= n & i <= n + 6 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is n,s integer holds

S2 is n,s integer

let s be set ; :: thesis: for S1, S2 being non empty BoolSignature st n >= 1 & the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= n + 6 & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & ( for i being Nat st i >= n & i <= n + 6 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is n,s integer holds

S2 is n,s integer

let S1, S2 be non empty BoolSignature ; :: thesis: ( n >= 1 & the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= n + 6 & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & ( for i being Nat st i >= n & i <= n + 6 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is n,s integer implies S2 is n,s integer )

assume A1: ( n >= 1 & the bool-sort of S1 = the bool-sort of S2 ) ; :: thesis: ( not len the connectives of S2 >= n + 6 or not the connectives of S2 . n <> the connectives of S2 . (n + 1) or not the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) or not the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) or not the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) or ex i being Nat st

( i >= n & i <= n + 6 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is n,s integer or S2 is n,s integer )

assume A2: len the connectives of S2 >= n + 6 ; :: thesis: ( not the connectives of S2 . n <> the connectives of S2 . (n + 1) or not the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) or not the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) or not the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) or ex i being Nat st

( i >= n & i <= n + 6 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is n,s integer or S2 is n,s integer )

assume A3: ( the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) ) ; :: thesis: ( ex i being Nat st

( i >= n & i <= n + 6 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is n,s integer or S2 is n,s integer )

assume A4: for i being Nat st i >= n & i <= n + 6 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ; :: thesis: ( not S1 is n,s integer or S2 is n,s integer )

assume len the connectives of S1 >= n + 6 ; :: according to AOFA_A00:def 38 :: thesis: ( for I being Element of S1 holds

( not I = s or not I <> the bool-sort of S1 or not the connectives of S1 . n is_of_type {} ,I or not the connectives of S1 . (n + 1) is_of_type {} ,I or not the connectives of S1 . n <> the connectives of S1 . (n + 1) or not the connectives of S1 . (n + 2) is_of_type <*I*>,I or not the connectives of S1 . (n + 3) is_of_type <*I,I*>,I or not the connectives of S1 . (n + 4) is_of_type <*I,I*>,I or not the connectives of S1 . (n + 5) is_of_type <*I,I*>,I or not the connectives of S1 . (n + 3) <> the connectives of S1 . (n + 4) or not the connectives of S1 . (n + 3) <> the connectives of S1 . (n + 5) or not the connectives of S1 . (n + 4) <> the connectives of S1 . (n + 5) or not the connectives of S1 . (n + 6) is_of_type <*I,I*>, the bool-sort of S1 ) or S2 is n,s integer )

given I being Element of S1 such that A5: ( I = s & I <> the bool-sort of S1 & the connectives of S1 . n is_of_type {} ,I & the connectives of S1 . (n + 1) is_of_type {} ,I & the connectives of S1 . n <> the connectives of S1 . (n + 1) & the connectives of S1 . (n + 2) is_of_type <*I*>,I & the connectives of S1 . (n + 3) is_of_type <*I,I*>,I & the connectives of S1 . (n + 4) is_of_type <*I,I*>,I & the connectives of S1 . (n + 5) is_of_type <*I,I*>,I & the connectives of S1 . (n + 3) <> the connectives of S1 . (n + 4) & the connectives of S1 . (n + 3) <> the connectives of S1 . (n + 5) & the connectives of S1 . (n + 4) <> the connectives of S1 . (n + 5) & the connectives of S1 . (n + 6) is_of_type <*I,I*>, the bool-sort of S1 ) ; :: thesis: S2 is n,s integer

thus len the connectives of S2 >= n + 6 by A2; :: according to AOFA_A00:def 38 :: thesis: ex I being Element of S2 st

( I = s & I <> the bool-sort of S2 & the connectives of S2 . n is_of_type {} ,I & the connectives of S2 . (n + 1) is_of_type {} ,I & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*I*>,I & the connectives of S2 . (n + 3) is_of_type <*I,I*>,I & the connectives of S2 . (n + 4) is_of_type <*I,I*>,I & the connectives of S2 . (n + 5) is_of_type <*I,I*>,I & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*I,I*>, the bool-sort of S2 )

A6: n <= n + 6 by NAT_1:11;

then n <= len the connectives of S2 by A2, XXREAL_0:2;

then A7: n in dom the connectives of S2 by A1, FINSEQ_3:25;

A8: the ResultSort of S2 . ( the connectives of S2 . n) = the ResultSort of S1 . ( the connectives of S1 . n) by A4, A6

.= I by A5 ;

reconsider J = I as Element of S2 by A8, A7, FUNCT_2:5, FUNCT_1:102;

take J ; :: thesis: ( J = s & J <> the bool-sort of S2 & the connectives of S2 . n is_of_type {} ,J & the connectives of S2 . (n + 1) is_of_type {} ,J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus ( J = s & J <> the bool-sort of S2 ) by A1, A5; :: thesis: ( the connectives of S2 . n is_of_type {} ,J & the connectives of S2 . (n + 1) is_of_type {} ,J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the Arity of S2 . ( the connectives of S2 . n) = the Arity of S1 . ( the connectives of S1 . n) by A4, A6

.= {} by A5 ; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . n) = J & the connectives of S2 . (n + 1) is_of_type {} ,J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . n) = the ResultSort of S1 . ( the connectives of S1 . n) by A4, A6

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 1) is_of_type {} ,J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A9: ( n + 0 <= n + 1 & n + 1 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 1)) = the Arity of S1 . ( the connectives of S1 . (n + 1)) by A4

.= {} by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 1)) = J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 1)) = the ResultSort of S1 . ( the connectives of S1 . (n + 1)) by A4, A9

.= J by A5 ; :: thesis: ( the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the connectives of S2 . n <> the connectives of S2 . (n + 1) by A3; :: thesis: ( the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A10: ( n + 0 <= n + 2 & n + 2 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 2)) = the Arity of S1 . ( the connectives of S1 . (n + 2)) by A4

.= <*J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 2)) = J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 2)) = the ResultSort of S1 . ( the connectives of S1 . (n + 2)) by A4, A10

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A11: ( n + 0 <= n + 3 & n + 3 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 3)) = the Arity of S1 . ( the connectives of S1 . (n + 3)) by A4

.= <*J,J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 3)) = J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 3)) = the ResultSort of S1 . ( the connectives of S1 . (n + 3)) by A4, A11

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A12: ( n + 0 <= n + 4 & n + 4 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 4)) = the Arity of S1 . ( the connectives of S1 . (n + 4)) by A4

.= <*J,J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 4)) = J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 4)) = the ResultSort of S1 . ( the connectives of S1 . (n + 4)) by A4, A12

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A13: ( n + 0 <= n + 5 & n + 5 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 5)) = the Arity of S1 . ( the connectives of S1 . (n + 5)) by A4

.= <*J,J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 5)) = J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 5)) = the ResultSort of S1 . ( the connectives of S1 . (n + 5)) by A4, A13

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) by A3; :: thesis: ( the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) by A3; :: thesis: ( the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) by A3; :: thesis: the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2

A14: n + 0 <= n + 6 by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 6)) = the Arity of S1 . ( the connectives of S1 . (n + 6)) by A4

.= <*J,J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: the ResultSort of S2 . ( the connectives of S2 . (n + 6)) = the bool-sort of S2

thus the ResultSort of S2 . ( the connectives of S2 . (n + 6)) = the ResultSort of S1 . ( the connectives of S1 . (n + 6)) by A4, A14

.= the bool-sort of S2 by A1, A5 ; :: thesis: verum

for S1, S2 being non empty BoolSignature st n >= 1 & the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= n + 6 & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & ( for i being Nat st i >= n & i <= n + 6 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is n,s integer holds

S2 is n,s integer

let s be set ; :: thesis: for S1, S2 being non empty BoolSignature st n >= 1 & the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= n + 6 & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & ( for i being Nat st i >= n & i <= n + 6 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is n,s integer holds

S2 is n,s integer

let S1, S2 be non empty BoolSignature ; :: thesis: ( n >= 1 & the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= n + 6 & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & ( for i being Nat st i >= n & i <= n + 6 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is n,s integer implies S2 is n,s integer )

assume A1: ( n >= 1 & the bool-sort of S1 = the bool-sort of S2 ) ; :: thesis: ( not len the connectives of S2 >= n + 6 or not the connectives of S2 . n <> the connectives of S2 . (n + 1) or not the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) or not the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) or not the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) or ex i being Nat st

( i >= n & i <= n + 6 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is n,s integer or S2 is n,s integer )

assume A2: len the connectives of S2 >= n + 6 ; :: thesis: ( not the connectives of S2 . n <> the connectives of S2 . (n + 1) or not the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) or not the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) or not the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) or ex i being Nat st

( i >= n & i <= n + 6 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is n,s integer or S2 is n,s integer )

assume A3: ( the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) ) ; :: thesis: ( ex i being Nat st

( i >= n & i <= n + 6 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is n,s integer or S2 is n,s integer )

assume A4: for i being Nat st i >= n & i <= n + 6 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ; :: thesis: ( not S1 is n,s integer or S2 is n,s integer )

assume len the connectives of S1 >= n + 6 ; :: according to AOFA_A00:def 38 :: thesis: ( for I being Element of S1 holds

( not I = s or not I <> the bool-sort of S1 or not the connectives of S1 . n is_of_type {} ,I or not the connectives of S1 . (n + 1) is_of_type {} ,I or not the connectives of S1 . n <> the connectives of S1 . (n + 1) or not the connectives of S1 . (n + 2) is_of_type <*I*>,I or not the connectives of S1 . (n + 3) is_of_type <*I,I*>,I or not the connectives of S1 . (n + 4) is_of_type <*I,I*>,I or not the connectives of S1 . (n + 5) is_of_type <*I,I*>,I or not the connectives of S1 . (n + 3) <> the connectives of S1 . (n + 4) or not the connectives of S1 . (n + 3) <> the connectives of S1 . (n + 5) or not the connectives of S1 . (n + 4) <> the connectives of S1 . (n + 5) or not the connectives of S1 . (n + 6) is_of_type <*I,I*>, the bool-sort of S1 ) or S2 is n,s integer )

given I being Element of S1 such that A5: ( I = s & I <> the bool-sort of S1 & the connectives of S1 . n is_of_type {} ,I & the connectives of S1 . (n + 1) is_of_type {} ,I & the connectives of S1 . n <> the connectives of S1 . (n + 1) & the connectives of S1 . (n + 2) is_of_type <*I*>,I & the connectives of S1 . (n + 3) is_of_type <*I,I*>,I & the connectives of S1 . (n + 4) is_of_type <*I,I*>,I & the connectives of S1 . (n + 5) is_of_type <*I,I*>,I & the connectives of S1 . (n + 3) <> the connectives of S1 . (n + 4) & the connectives of S1 . (n + 3) <> the connectives of S1 . (n + 5) & the connectives of S1 . (n + 4) <> the connectives of S1 . (n + 5) & the connectives of S1 . (n + 6) is_of_type <*I,I*>, the bool-sort of S1 ) ; :: thesis: S2 is n,s integer

thus len the connectives of S2 >= n + 6 by A2; :: according to AOFA_A00:def 38 :: thesis: ex I being Element of S2 st

( I = s & I <> the bool-sort of S2 & the connectives of S2 . n is_of_type {} ,I & the connectives of S2 . (n + 1) is_of_type {} ,I & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*I*>,I & the connectives of S2 . (n + 3) is_of_type <*I,I*>,I & the connectives of S2 . (n + 4) is_of_type <*I,I*>,I & the connectives of S2 . (n + 5) is_of_type <*I,I*>,I & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*I,I*>, the bool-sort of S2 )

A6: n <= n + 6 by NAT_1:11;

then n <= len the connectives of S2 by A2, XXREAL_0:2;

then A7: n in dom the connectives of S2 by A1, FINSEQ_3:25;

A8: the ResultSort of S2 . ( the connectives of S2 . n) = the ResultSort of S1 . ( the connectives of S1 . n) by A4, A6

.= I by A5 ;

reconsider J = I as Element of S2 by A8, A7, FUNCT_2:5, FUNCT_1:102;

take J ; :: thesis: ( J = s & J <> the bool-sort of S2 & the connectives of S2 . n is_of_type {} ,J & the connectives of S2 . (n + 1) is_of_type {} ,J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus ( J = s & J <> the bool-sort of S2 ) by A1, A5; :: thesis: ( the connectives of S2 . n is_of_type {} ,J & the connectives of S2 . (n + 1) is_of_type {} ,J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the Arity of S2 . ( the connectives of S2 . n) = the Arity of S1 . ( the connectives of S1 . n) by A4, A6

.= {} by A5 ; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . n) = J & the connectives of S2 . (n + 1) is_of_type {} ,J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . n) = the ResultSort of S1 . ( the connectives of S1 . n) by A4, A6

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 1) is_of_type {} ,J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A9: ( n + 0 <= n + 1 & n + 1 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 1)) = the Arity of S1 . ( the connectives of S1 . (n + 1)) by A4

.= {} by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 1)) = J & the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 1)) = the ResultSort of S1 . ( the connectives of S1 . (n + 1)) by A4, A9

.= J by A5 ; :: thesis: ( the connectives of S2 . n <> the connectives of S2 . (n + 1) & the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the connectives of S2 . n <> the connectives of S2 . (n + 1) by A3; :: thesis: ( the connectives of S2 . (n + 2) is_of_type <*J*>,J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A10: ( n + 0 <= n + 2 & n + 2 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 2)) = the Arity of S1 . ( the connectives of S1 . (n + 2)) by A4

.= <*J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 2)) = J & the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 2)) = the ResultSort of S1 . ( the connectives of S1 . (n + 2)) by A4, A10

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 3) is_of_type <*J,J*>,J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A11: ( n + 0 <= n + 3 & n + 3 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 3)) = the Arity of S1 . ( the connectives of S1 . (n + 3)) by A4

.= <*J,J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 3)) = J & the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 3)) = the ResultSort of S1 . ( the connectives of S1 . (n + 3)) by A4, A11

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 4) is_of_type <*J,J*>,J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A12: ( n + 0 <= n + 4 & n + 4 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 4)) = the Arity of S1 . ( the connectives of S1 . (n + 4)) by A4

.= <*J,J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 4)) = J & the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 4)) = the ResultSort of S1 . ( the connectives of S1 . (n + 4)) by A4, A12

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 5) is_of_type <*J,J*>,J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

A13: ( n + 0 <= n + 5 & n + 5 <= n + 6 ) by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 5)) = the Arity of S1 . ( the connectives of S1 . (n + 5)) by A4

.= <*J,J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . (n + 5)) = J & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . (n + 5)) = the ResultSort of S1 . ( the connectives of S1 . (n + 5)) by A4, A13

.= J by A5 ; :: thesis: ( the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) & the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 4) by A3; :: thesis: ( the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the connectives of S2 . (n + 3) <> the connectives of S2 . (n + 5) by A3; :: thesis: ( the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) & the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2 )

thus the connectives of S2 . (n + 4) <> the connectives of S2 . (n + 5) by A3; :: thesis: the connectives of S2 . (n + 6) is_of_type <*J,J*>, the bool-sort of S2

A14: n + 0 <= n + 6 by XREAL_1:6;

hence the Arity of S2 . ( the connectives of S2 . (n + 6)) = the Arity of S1 . ( the connectives of S1 . (n + 6)) by A4

.= <*J,J*> by A5 ;

:: according to AOFA_A00:def 8 :: thesis: the ResultSort of S2 . ( the connectives of S2 . (n + 6)) = the bool-sort of S2

thus the ResultSort of S2 . ( the connectives of S2 . (n + 6)) = the ResultSort of S1 . ( the connectives of S1 . (n + 6)) by A4, A14

.= the bool-sort of S2 by A1, A5 ; :: thesis: verum