let S be non empty non void ManySortedSign ; for V being non-empty ManySortedSet of the carrier of S
for X1, X2 being non empty Subset of (S -Terms V) holds
( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) )
let V be non-empty ManySortedSet of the carrier of S; for X1, X2 being non empty Subset of (S -Terms V) holds
( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) )
let t1, t2 be non empty Subset of (S -Terms V); ( the Arity of (t1 -CircuitStr) tolerates the Arity of (t2 -CircuitStr) & the ResultSort of (t1 -CircuitStr) tolerates the ResultSort of (t2 -CircuitStr) )
set C = [: the carrier' of S,{ the carrier of S}:];
A1:
dom ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t1) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t1
by FUNCT_2:def 1;
A2:
dom ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t2) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t2
by FUNCT_2:def 1;
hereby PARTFUN1:def 4 the ResultSort of (t1 -CircuitStr) tolerates the ResultSort of (t2 -CircuitStr)
let x be
object ;
( x in (dom the Arity of (t1 -CircuitStr)) /\ (dom the Arity of (t2 -CircuitStr)) implies the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . x )assume A3:
x in (dom the Arity of (t1 -CircuitStr)) /\ (dom the Arity of (t2 -CircuitStr))
;
the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . xthen A4:
x in dom the
Arity of
(t1 -CircuitStr)
by XBOOLE_0:def 4;
A5:
x in dom the
Arity of
(t2 -CircuitStr)
by A3, XBOOLE_0:def 4;
reconsider u =
x as
Element of
Subtrees t1 by A1, A4;
([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t1) . x in (Subtrees t1) *
by A1, A4, FUNCT_2:5;
then reconsider y1 = the
Arity of
(t1 -CircuitStr) . x as
FinSequence of
Subtrees t1 by FINSEQ_1:def 11;
the
Arity of
(t2 -CircuitStr) . x in (Subtrees t2) *
by A2, A5, FUNCT_2:5;
then reconsider y2 = the
Arity of
(t2 -CircuitStr) . x as
FinSequence of
Subtrees t2 by FINSEQ_1:def 11;
A6:
( ( for
t being
Element of
t1 holds
t is
finite ) & ( for
t being
Element of
t2 holds
t is
finite ) )
;
then A7:
u = (u . {}) -tree y1
by A1, A4, TREES_9:def 13;
u = (u . {}) -tree y2
by A2, A5, A6, TREES_9:def 13;
hence
the
Arity of
(t1 -CircuitStr) . x = the
Arity of
(t2 -CircuitStr) . x
by A7, TREES_4:15;
verum
end;
let x be object ; PARTFUN1:def 4 ( not x in (proj1 the ResultSort of (t1 -CircuitStr)) /\ (proj1 the ResultSort of (t2 -CircuitStr)) or the ResultSort of (t1 -CircuitStr) . x = the ResultSort of (t2 -CircuitStr) . x )
assume A8:
x in (dom the ResultSort of (t1 -CircuitStr)) /\ (dom the ResultSort of (t2 -CircuitStr))
; the ResultSort of (t1 -CircuitStr) . x = the ResultSort of (t2 -CircuitStr) . x
then A9:
x in dom the ResultSort of (t1 -CircuitStr)
by XBOOLE_0:def 4;
A10:
x in dom the ResultSort of (t2 -CircuitStr)
by A8, XBOOLE_0:def 4;
thus the ResultSort of (t1 -CircuitStr) . x =
x
by A9, FUNCT_1:18
.=
the ResultSort of (t2 -CircuitStr) . x
by A10, FUNCT_1:18
; verum