let x be Vertex of S; :: thesis: for v being Element of V . x ex a being Element of the Sorts of A . x st S₁[x,v,a]
let v be Element of V . x; :: thesis: ex a being Element of the Sorts of A . x st S₁[x,v,a]

per cases ( not root-tree [v,x] in Subtrees X or root-tree [v,x] in Subtrees X ) ;

suppose not root-tree [v,x] in Subtrees X ; :: thesis: ex a being Element of the Sorts of A . x st S₁[x,v,a]

hence ex a being Element of the Sorts of A . x st S₁[x,v,a] ; :: thesis: verum

end;

suppose root-tree [v,x] in Subtrees X ; :: thesis: ex a being Element of the Sorts of A . x st S₁[x,v,a]

then reconsider a = root-tree [v,x] as Vertex of (X -CircuitStr) ;
reconsider t = a as Term of S,V by MSATERM:4;
A2: the_sort_of t = x by MSATERM:14;
A3: the_sort_of (a,A) = the Sorts of A . (the_sort_of t) by Def2;
(X -CircuitSorts A) . a = the_sort_of (a,A) by Def4;
then reconsider b = s . a as Element of the Sorts of A . x by A2, A3, CIRCUIT1:4;
take b ; :: thesis: S₁[x,v,b]
thus S₁[x,v,b] ; :: thesis: verum

end;

end;