let it1, it2 be strict ConstructorSignature; :: thesis: ( the carrier' of it1 = {*,non_op} \/ Constructors & ( for o being OperSymbol of it1 st o is constructor holds
( the ResultSort of it1 . o = o `1 & card ( the Arity of it1 . o) = card ((o `2) `1) ) ) & the carrier' of it2 = {*,non_op} \/ Constructors & ( for o being OperSymbol of it2 st o is constructor holds
( the ResultSort of it2 . o = o `1 & card ( the Arity of it2 . o) = card ((o `2) `1) ) ) implies it1 = it2 )
assume that
A23: the carrier' of it1 = {*,non_op} \/ Constructors and
A24: for o being OperSymbol of it1 st o is constructor holds
( the ResultSort of it1 . o = o `1 & card ( the Arity of it1 . o) = card ((o `2) `1) ) and
A25: the carrier' of it2 = {*,non_op} \/ Constructors and
A26: for o being OperSymbol of it2 st o is constructor holds
( the ResultSort of it2 . o = o `1 & card ( the Arity of it2 . o) = card ((o `2) `1) ) ; :: thesis: it1 = it2
set S = {a_Type,an_Adj,a_Term};
A27: the carrier of it1 = {a_Type,an_Adj,a_Term} by Def9;
A28: the carrier of it2 = {a_Type,an_Adj,a_Term} by Def9;
A29: now :: thesis: for c being Element of Constructors st c <> * & c <> non_op holds
the Arity of it1 . c = the Arity of it2 . c
let c be Element of Constructors ; :: thesis: ( c <> * & c <> non_op implies the Arity of it1 . c = the Arity of it2 . c )
reconsider o1 = c as OperSymbol of it1 by A23, XBOOLE_0:def 3;
reconsider o2 = o1 as OperSymbol of it2 by A23, A25;
assume that
A30: c <> * and
A31: c <> non_op ; :: thesis: the Arity of it1 . c = the Arity of it2 . c
A32: o1 is constructor by A30, A31;
A33: o2 is constructor by A30, A31;
A34: card ( the Arity of it1 . o1) = card ((c `2) `1) by A24, A32;
A35: card ( the Arity of it2 . o2) = card ((c `2) `1) by A26, A33;
A36: the Arity of it1 . o1 in {a_Term} * by A30, A31, Def9;
the Arity of it2 . o2 in {a_Term} * by A30, A31, Def9;
then reconsider p1 = the Arity of it1 . o1, p2 = the Arity of it2 . o2 as FinSequence of {a_Term} by A36, FINSEQ_1:def 11;
A37: dom p1 = Seg (len p1) by FINSEQ_1:def 3;
A38: dom p2 = Seg (len p2) by FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in dom p1 holds
p1 . i = p2 . i
let i be Nat; :: thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume A39: i in dom p1 ; :: thesis: p1 . i = p2 . i
then A40: p1 . i in rng p1 by FUNCT_1:def 3;
A41: p2 . i in rng p2 by A34, A35, A37, A38, A39, FUNCT_1:def 3;
p1 . i = a_Term by A40, TARSKI:def 1;
hence p1 . i = p2 . i by A41, TARSKI:def 1; :: thesis: verum
end;
hence the Arity of it1 . c = the Arity of it2 . c by A34, A35, A37, A38; :: thesis: verum
end;
now :: thesis: for o being OperSymbol of it1 holds the Arity of it1 . o = the Arity of it2 . o
let o be OperSymbol of it1; :: thesis: the Arity of it1 . o = the Arity of it2 . o
( o in {*,non_op} or not o in {*,non_op} ) ;
then ( o = * or o = non_op or ( o in Constructors & o <> * & o <> non_op ) ) by A23, TARSKI:def 2, XBOOLE_0:def 3;
then ( ( the Arity of it1 . o = <*an_Adj,a_Type*> & the Arity of it2 . o = <*an_Adj,a_Type*> ) or ( the Arity of it1 . o = <*an_Adj*> & the Arity of it2 . o = <*an_Adj*> ) or the Arity of it1 . o = the Arity of it2 . o ) by A29, Def9;
hence the Arity of it1 . o = the Arity of it2 . o ; :: thesis: verum
end;
then A42: the Arity of it1 = the Arity of it2 by A23, A25, A27, A28, FUNCT_2:63;
now :: thesis: for o being OperSymbol of it1 holds the ResultSort of it1 . o = the ResultSort of it2 . o
let o be OperSymbol of it1; :: thesis: the ResultSort of it1 . o = the ResultSort of it2 . o
reconsider o9 = o as OperSymbol of it2 by A23, A25;
( not o in {*,non_op} or o in {*,non_op} ) ;
then ( o = * or o = non_op or ( o in Constructors & o is constructor & o9 is constructor ) ) by A23, TARSKI:def 2, XBOOLE_0:def 3;
then ( ( the ResultSort of it1 . o = a_Type & the ResultSort of it2 . o = a_Type ) or ( the ResultSort of it1 . o = an_Adj & the ResultSort of it2 . o = an_Adj ) or ( the ResultSort of it1 . o = o `1 & the ResultSort of it2 . o = o `1 ) ) by A24, A26, Def9;
hence the ResultSort of it1 . o = the ResultSort of it2 . o ; :: thesis: verum
end;
hence it1 = it2 by A23, A25, A27, A28, A42, FUNCT_2:63; :: thesis: verum