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