let L be non trivial multLoopStr_0 ; :: thesis: for z being rational_function of L holds z = [(z `1),(z `2)]
let z be rational_function of L; :: thesis: z = [(z `1),(z `2)]
consider p1 being Polynomial of L such that
A1: ex p2 being non zero Polynomial of L st z = [p1,p2] by Def8;
consider p2 being non zero Polynomial of L such that
A2: z = [p1,p2] by A1;
thus z = [(z `1),(z `2)] by A2; :: thesis: verum