let g1, g2 be Function; :: thesis: ( ex f being ManySortedFunction of NAT st
( g1 = f . (len p) & f . 0 = id X & ( for i being Nat st i + 1 in dom p holds
for g, h being Function st g = f . i & h = p . (i + 1) holds
f . (i + 1) = h * g ) ) & ex f being ManySortedFunction of NAT st
( g2 = f . (len p) & f . 0 = id X & ( for i being Nat st i + 1 in dom p holds
for g, h being Function st g = f . i & h = p . (i + 1) holds
f . (i + 1) = h * g ) ) implies g1 = g2 )
given f1 being ManySortedFunction of NAT such that A1: g1 = f1 . (len p) and
A2: f1 . 0 = id X and
A3: for i being Nat st i + 1 in dom p holds
for g, h being Function st g = f1 . i & h = p . (i + 1) holds
f1 . (i + 1) = h * g ; :: thesis: ( for f being ManySortedFunction of NAT holds
( not g2 = f . (len p) or not f . 0 = id X or ex i being Nat st
( i + 1 in dom p & ex g, h being Function st
( g = f . i & h = p . (i + 1) & not f . (i + 1) = h * g ) ) ) or g1 = g2 )
given f2 being ManySortedFunction of NAT such that A4: g2 = f2 . (len p) and
A5: f2 . 0 = id X and
A6: for i being Nat st i + 1 in dom p holds
for g, h being Function st g = f2 . i & h = p . (i + 1) holds
f2 . (i + 1) = h * g ; :: thesis: g1 = g2
defpred S₁[ Nat] means ( $1 <= len p implies ( f1 . $1 = f2 . $1 & f1 . $1 is Function ) );
A7: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A8: ( i <= len p implies ( f1 . i = f2 . i & f1 . i is Function ) ) and
A9: i + 1 <= len p ; :: thesis: ( f1 . (i + 1) = f2 . (i + 1) & f1 . (i + 1) is Function )
reconsider h = p . (i + 1) as Function ;
reconsider g = f1 . i as Function ;
i + 1 >= 1 by NAT_1:11;
then A10: i + 1 in dom p by A9, FINSEQ_3:25;
then f1 . (i + 1) = h * g by A3;
hence ( f1 . (i + 1) = f2 . (i + 1) & f1 . (i + 1) is Function ) by A6, A8, A9, A10, NAT_1:13; :: thesis: verum

end;

A11: S₁[ 0 ] by A2, A5;
for i being Nat holds S₁[i] from NAT_1:sch 2(A11, A7);
hence g1 = g2 by A1, A4; :: thesis: verum