let n be Nat; 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 ; 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 ; ( 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 )
; ( 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
; ( 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) )
; ( 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) )
; ( not S1 is n,s integer or S2 is n,s integer )
assume
len the connectives of S1 >= n + 6
; AOFA_A00:def 38 ( 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 )
; S2 is n,s integer
thus
len the connectives of S2 >= n + 6
by A2; AOFA_A00:def 38 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
; ( 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; ( 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
; AOFA_A00:def 8 ( 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
; ( 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
;
AOFA_A00:def 8 ( 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
; ( 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; ( 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
;
AOFA_A00:def 8 ( 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
; ( 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
;
AOFA_A00:def 8 ( 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
; ( 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
;
AOFA_A00:def 8 ( 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
; ( 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
;
AOFA_A00:def 8 ( 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
; ( 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; ( 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; ( 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; 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
;
AOFA_A00:def 8 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
; verum