let S be non empty non void ManySortedSign ; for V being V5() 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 V5() 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 (id ([:the carrier' of S,{the carrier of S}:] -Subtrees t1)) = [:the carrier' of S,{the carrier of S}:] -Subtrees t1
by RELAT_1:71;
A3:
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;
A4:
dom (id ([:the carrier' of S,{the carrier of S}:] -Subtrees t2)) = [:the carrier' of S,{the carrier of S}:] -Subtrees t2
by RELAT_1:71;
hereby PARTFUN1:def 6 the ResultSort of (t1 -CircuitStr ) tolerates the ResultSort of (t2 -CircuitStr )
let x be
set ;
( 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 A5:
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 A6:
x in dom the
Arity of
(t1 -CircuitStr )
by XBOOLE_0:def 4;
A7:
x in dom the
Arity of
(t2 -CircuitStr )
by A5, XBOOLE_0:def 4;
reconsider u =
x as
Element of
Subtrees t1 by A1, A6;
([:the carrier' of S,{the carrier of S}:] -ImmediateSubtrees t1) . x in (Subtrees t1) *
by A1, A6, FUNCT_2:7;
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 A3, A7, FUNCT_2:7;
then reconsider y2 = the
Arity of
(t2 -CircuitStr ) . x as
FinSequence of
Subtrees t2 by FINSEQ_1:def 11;
A8:
( ( for
t being
Element of
t1 holds
t is
finite ) & ( for
t being
Element of
t2 holds
t is
finite ) )
;
then A9:
u = (u . {} ) -tree y1
by A1, A6, TREES_9:def 13;
u = (u . {} ) -tree y2
by A3, A7, A8, TREES_9:def 13;
hence
the
Arity of
(t1 -CircuitStr ) . x = the
Arity of
(t2 -CircuitStr ) . x
by A9, TREES_4:15;
verum
end;
let x be set ; PARTFUN1:def 6 ( 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 A10:
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 A11:
x in dom the ResultSort of (t1 -CircuitStr )
by XBOOLE_0:def 4;
A12:
x in dom the ResultSort of (t2 -CircuitStr )
by A10, XBOOLE_0:def 4;
thus the ResultSort of (t1 -CircuitStr ) . x =
x
by A2, A11, FUNCT_1:35
.=
the ResultSort of (t2 -CircuitStr ) . x
by A4, A12, FUNCT_1:35
; verum